\chapter{Progress Report 1}
\label{progrep1-chap}
\section{Project Description}

Extended ML (EML) is a specification language based on the
modularisation facilities provided by the Standard ML (SML) programming
language. EML can be user to express every stage in the development of
a SML program from the initial high-level specification to the final
program itself and including intermediate stages in which
specification and program are intermingled. Programs are evolved from
specifications in EML in a series of refinement steps in which
high-level specifications are replaced by lower-level specifications.
This leads ultimately to a specification expressed entirely in the
executable subset of EML, ie. to a SML program. If every refinement
step is proved correct then the program which results is guaranteed to
be correct with respect to the original specification.

The project will contribute to tool support for EML. By the time the
project begins, an EML parser and typechecker will be available. The
first goal of this project will be to provide a tools which generates
the proof obligations incurred in the course of formal program
development in EML. Each refinement step gives rise to a certain
number of proof obligations of the form \(SP\models SP'\) where \(SP\) and \(SP'\) are
EML structures or signatures which may contain axioms; discharging
these (showing that they are in fact theorems) establishes the
correctness of that step. Many (in fact most) of the proof
obligations which arise in practice are trivial or almost trivial,
meaning that they can be discharged by syntactic means without
recourse to theorem proving techniques. It is desirable to eliminate
these, leaving the developer with the task of discharging the
non-trivial proof obligations with the help of an interactive theorem
prover. This project will develop methods for eliminating trivial
proof obligations; if there is time, experiments will be carried out
using an existing theorem prover (eg. LEGO) to discharge non-trivial
proof obligations.


We will use the entailment symbol \(\models\) as a relation over signatures. If
a signature (specification) \(SP\) entails another \(SP'\) then we will write
\(SP \models SP'\). We take this to mean that any structure matching the
signature SP is a suitable candidate to match the structure \(SP'\). There
are two requirements here. First, the signatures \(SP'\) and \(SP\) must type
match and secondly, all the axioms in \(SP'\) (ie. the specification
requirements) must be shown to be satisfied by those in \(SP\).

Primarily, the project is concerned with the axiomatic obligations.
The type-checking is an integral part of the EML typechecker which now
exists. 

Consider the EML development process from high level specification to
low level implementation in SML code. The development steps allowed at
each stage are of three identifiable kinds (as in \cite{San90}).

\begin{enumerate}
\item Decomposition step. A functor is implemented as a composition of
"lesser" functors, which are then separately developed. This is a
standard divide-and-conquer approach. In general, a functor
\(F(X:IN):OUT=?\) can be implemented in terms of \(n\) functors \(G1,G2....Gn\) as
long as certain requirements are met. However, this general
decomposition can be viewed in terms of a simpler decomposition step
for which the proof obligations are clear.

Consider a functor \(F(X:IN):OUT=?\) We choose to implement \(F\) in terms of
functor \(G(X:GIN):GOUT=?\) and functor \(H(X:HIN):HOUT=?\), so we have
functor \(F(X:IN):OUT=H(G(X))\). Now, the proof obligations for this step
(apart from the typechecking) are:
\(IN \models GIN, GOUT \models HIN, HOUT \models OUT\)

\item Coding step. A functor body is provided in abstract form
(containing type and value declarations and a mixture of axioms and
code to define them). A functor \(F(X:IN):OUT=?\) is replaced by the
definition \(F(X:IN):OUT=strexp\) where \(strexp\) is a well-formed EML
functor body. Typechecking aside, a single proof obligation is
incurred:
\(IN \cup strexp \models OUT\)

\item Refinement step. An abstract program is further refined to a more
concrete version which addresses some of the decisions left open by
the abstract version. A functor \(F(X:IN):OUT=strexp\) is replaced by the
definition functor \(F(X:IN):OUT=strexp'\). Again, we have a single proof
obligation: (excusing a slight abuse of the notation)
\(IN \cup strexp' \models strexp\)
We can see, however that this step, can easily be viewed as a coding
step (disregarding the refinements that have gone before).

\end {enumerate}

The project then is concerned with identifying the obligations and
presenting them to the developer (or in a form suitable for direct
input to a theorem prover). In general, we are trying to present the
obligations as a pair \((axiom, context)\) where \(axiom\) is the theorem that
requires ratification and \(context\) is the environment (containing
current theories, structure, signature and functor definitions).

As the EML parser, typechecker and interpreter now exist, I am trying
to closely ally the obligation generator to it so that the two can
combine to offer an integrated development environment. In fact,
without some form of make system, this would not make a great deal of
sense for any reasonable EML developments. But the SML
library provides such a system (\cite{Ber91}).

\section{Progress}

Initially, time was invested in developing an understanding of SML
syntax, semantics (static and dynamic) (\cite{HMM86}, \cite{HMT89}, \cite{MT90}), and the
syntax, semantics (static, dynamic and verification) of EML
(\cite{SdST92}). A grounding in the theory of algebraic specification and
its application to EML (\cite{ST89}, \cite{ST92}) was 
attained before an investigation into the construction of the EML
parser, typechecker and interpreter (undocumented, as yet).

With this knowledge, I have defined suitable interfaces to the EML
compiler and identified useful fragments of the compiler which I
require.

For development steps of type 1, I have code to identify the axioms,
their context and to syntactically match trivial obligations. At least
to a first order approximation, this section is complete. The form of
presentation of the obligations is not yet settled, so currently they
are presented in a human readable form.

\section{Future}

I will proceed with the project by turning my attention to the
remaining two types of development step. I envisage that I will treat
type 3 as a case of type 2. These two types of step are rather more
involved with the semantic objects used to represent functors,
structures and values. The work for type 1 has mostly been at a
syntactic level, with some recourse to the semantic objects.

Beyond this, there is plenty of scope for the consideration of
observable equivalence where the obligations generated are proved with
respect to an observable set of types ie. only those aspects of the
specification that can lead to discernible properties are proved. See
\cite{ST89}.

