The Formal Development of an SML Program Using the LEGO Theorem-Prover

Citation

Maharaj S (1991) The Formal Development of an SML Program Using the LEGO Theorem-Prover. Bell Labs.

Abstract
This report describes an attempt to used the Lego theorem-prover to develop a program in SML. Our aim is to use the theorem-prover as a uniform environment in which to express a specification, encode an implementation, and then verify that the specification is satisfied by the implementation. In particular, we would like to make use of certain constructs in the type system of the theorem-prover as mechanisms for expressing modularity in both the specification and the program. This work was carried out under the supervision of Elsa Gunter while the author was visiting Bell Laboratories in the summer of 1991 as a participant in the University Relations programme. I expressed a program specification in the Lego system. I then wrote an ML program which I translated into Lego, after which I formally proved that the translated program satisfied the specification. The specification describes a functor which takes as input a structure consisting of a ground type with an equality relation on the elements of the type, and returns a structure consisting of the ground type and its equality, a type of sets over the ground type and a collection of functions which operate on these sets, such as union, intersection and so forth.