Verifying Specified Programs

The objective of the project was to investigate the territory between two strands of research in an attempt to bring them closer together:

• Work on type theory as a basis for computer-assisted formal reasoning, and specifically the Lego proof development system and its applications.
• Work on algebraic specification, and specifically the Extended ML framework for specification and formal development of modular Standard ML programs.

Some particularly noteworthy achievements were as follows.

• Pre-logical relations: A weakening of the important and widely-used concept of logical relations was studied. These have many of the features that make logical relations so useful as well as further algebraic properties including composability. This is the minimal weakening of logical relations giving composability and the most liberal definition that gives the Basic Lemma, which is the key to most applications of logical relations. Using pre-logical relations in place of logical relations can give improved results: for instance, Mitchell's characterisation of observational equivalence in terms of logical relations need not be restricted to first-order signatures.
• Domain-specific languages: The use of diagrammatic representations in DSLs and the potential that such representations hold for easing verification and reasoning tasks were investigated in the context of IEC 1131-3, an industry standard programming language for embedded control systems.
• Specification refinement: An elegant unification of approaches from algebraic specification and type theory was obtained by expressing a general notion of refinement from algebraic specification in System F, where specifications are expressed using existential types, and using a logic augmented with axioms postulating relational parametricity and existence of quotients and sub-objects.
• ML modules: A production-quality implementation of a powerful and soundly-based extension of the ML module system was produced, with an accompanying semantic description. The extensions support higher-order modules, separate compilation and first-class modules.
• Hoare logic in Lego: Proofs of soundness and completeness of Hoare Logic for imperative programs with recursive procedures were developed in Lego, uncovering errors in published proofs and stimulating improved versions of the rules, especially in connection with auxiliary variables.