This thesis presents a novel application of the technique known as proofs-as-programs. Proofs-as-programs defines a correspondence between proofs in a constructive logic and fundamental programs. By using this correspondence, a functional program may be represented directly as the proof of a specification and so the program may be analysed, within this proof framework. <I>C<SUP>Y</SUP>NTHIA</I> is a programming editor for the functional language ML which uses proofs-as-programs to analyse users' programs as they are written. So that the user requires no knowledge of proof theory, the underlying proof representation is completely hidden. The proof framework allows programs written in <I>C<SUP>Y</SUP>NTHIA </I>to be checked to be syntactically correct, well-typed, well-defined and terminating. Users of <I>C<SUP>Y</SUP>NTHIA</I> make fewer programming errors and the feedback facilities of <I>C<SUP>Y</SUP>NTHIA</I> mean that it is easier to track down the source of errors when they do occur. <I>C<SUP>Y</SUP>NTHIA</I> also embodies the idea of programming by analogy - rather than starting from scratch, users always begin with an existing function definition. They then apply a sequence of high-level editing commands which transform this starting definition into the one required. These commands preserve correctness and also increase programming efficiency by automating commonly occurring steps. The thesis describes the design and implementation of <I>C<SUP>Y</SUP>NTHIA</I> and investigates its role as a novice programming environment. Use by experts is possible but only a subset of ML is currently supported. Two major trials of <I>C<SUP>Y</SUP>NTHIA</I> have shown that <I>C<SUP>Y</SUP>NTHIA</I> is well-suited as a teaching tool.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:663736 |
| Date | January 1999 |
| Creators | Whittle, J. N. D. |
| Publisher | University of Edinburgh |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0022 seconds