This describes Ianthe Hind's fouth year honours project.
Cynthia is an ML based editor written by Jonathan Whittle as part of his 1998 PhD thesis entitles "The use of proofs-as-programs to build an analogy based functional programming editor".
Cynthia uses proofs-as-programs in order validate functions written within as they are being written. Cynthia proved useful in trials run in two ML courses at Napier University.
Paul Martin took a fresh look at Cynthia in 2004/2005 as part of his honours dissertation entitled "Exploring and Extending the Capabilities of Cynthia".
The result was a program called Anastasia whose implementation was based around some of the ideas behind Cynthia, but with some distinctly different characteristics and objectives.
Anastasia was designed to support an unlimited number of programming languages as opposed to Cynthia which worked over a specific subset of Standard ML.
There are numerous directions that can be taken to improve and upgrade Anastasia. The areas of interest for this project are now given.
There has been a resurgence of interest in functional programming, particularly in Haskell, within the School of Informatics at Edinburgh University. Haskell is now being taught to first year Informatics students and this provides a perfect opportunity to run student trials to evaluate the usefulness of Anastasia. A language script for Haskell needs to be written for Anastasia to allow these evaluations to take place.
Anastasia was designed and implemented to provide most of the core functionality of Cynthia, as well as emulate some of its formal verification capabilities. Cynthia performed termination checking on a large subset of recursive functions using Walther Recursion. It will be investigated how this method could be applied to Anastasia as well as other methods such as Recursive Path Orderings.
Student evaluations of Anastasia are planned to take place after the design and implementation of these extensions are completed. The evaluations will look at Anastasia as a whole, hopefully validating some of the arguments made in Paul's dissertation.
Write a context-free grammar for Haskell in the format of Anastasia's language scripts
Write documentation for Anastasia for use by Students.
Perform student evaluations of Anastasia giving a thorough analysis of the usefulness of such a formal-method guided functional programming editor
Please click here
to download a copy of Ianthe's
Back to Main
The following people are assosciated with the Anastasia project: