MRG home page · Research · Publications · Projects · Software · People

Extending the Capabilities of Anastasia

This describes Ianthe Hind's fouth year honours project.

Background

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.

Project Description

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.

Project Goals

  • 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
  • Project Report

    Please click here to download a copy of Ianthe's Dissertation.

    Back to Main

    People

    The following people are assosciated with the Anastasia project:

    Alan Bundy [A.Bundy@ed.ac.uk]Supervisor 
    Paul Martin [P.W.Martin@sms.ed.ac.uk]Second Supervisor 
    Ianthe Hind [I.Hind@sms.ed.ac.uk]Honours Student (2005-06) 
    Sebin Kim [S.Kim-11@sms.ed.ac.uk]Honours Student (2007-08) 

    Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
    Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
    Please send corrections and suggestions for this page to the DReaM Support Team
    Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.