The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

MSc Thesis #9803

Title:A Java editor based on proofs-as-programs
Date: 1998
Abstract:This thesis investigates the proofs-as-programs paradigm for the creation of Java code. It uses the Oyster proof planner and is based on the work of Jon Whittle for his CYNTHIA system.Jcyn is a development environment for Java code. The user creates code via a graphical user interface, and edits with a number of predefined editing commands. Code may be created from nothing or existing code from a library may be modified (known as programming by analogy).Although the user works with the code via a GUI, the underlying system uses a hiden proof engine to represent and manipulate the code. Edits to the program are translated and sent to the proof engine for processing, after which the code is extracted from the proof engine and redisplayed to the user.Because the code is manipulated with a proof engine, code can be automatically or semi-automatically generated (known as program synthesis) and certain properties of the program can be guaranteed.

[Search These Pages] [DAI Home Page] [Comment]