\chapter{Progress Report 2}
\label{progrep2-chap}
To be read in conjunction with progress report 1. Particularly, see
initial project description.

\section{Changes since Progress Report 1}

Influenced by pre-empting the task of integrating with the Kit
Compiler and problems encountered in dealing with local and open
constructs, my analysis of EML code has changed nature from an
absolute analysis to an incremental one so each syntactic clause
leads to some increments to the current verification basis. This is
more allied to the static and dynamic semantics for EML and makes for
a more intuitive analysis.

My first impression was that by treating refinement steps as coding
steps, I could a) simplify the system b) retain all development power.
While no extra possibilities for development arise from refinement
steps, they are an important element of the methodology and it turns
out that procedures for analysis of coding steps can be adjusted to
deal with refinement steps in a fairly straightforward way.

\section{Progress to date}

Code to deal with all three types of EML development step now exists.
My system provides an environment which manages signatures, structures
and functors, their associated axioms, and developments of these
objects. At the toplevel, given an EML syntax tree (type topdec), and
a current verification environment (type all-env), the system
provides a function
\begin{verbatim}
deal-with-topdec: topdec * all-env -> all-env * consequence
\end{verbatim}
where consequence is the type of a series of obligations and the
returned all-env is the updated verification basis.

\section{Stumbling block}

While all of the fundamental code to handle obligations for the three
types of development steps is complete, as yet I have not been able to
access semantic information from the Kit Compiler. Information is
required from both the static and dynamic analyses of EML programs.
From the static, type information (eg. to satisfy a `forall x:t ...'
obligation) and from the dynamic, value definitions for use in proofs.

The reason for this is that the Kit Compiler is not yet completed and
the dynamic semantics for the modules system has not been
implemented. However, it remains likely that a complete consistent
version will be available within a few days.

\section{Completion routes}

There remain a few essential tasks and numerous optional tasks to be
undertaken. Here is a description of them with a brief discussion of
their viability.

\begin{itemize}
\item Integration with Kit Compiler (Essential). Subject to the completion
of the Kit Compiler (see above), my system needs to be combined with
the compiler code. In particular, I need hooks into the compiler to
pick up selected static and dynamic semantic objects.

\item Documentation (Essential). I will have to develop some latex skills
and document production invariably takes longer than expected.
However, I have kept a record of project evolution, issues raised
and problems overcome. This will greatly aid the documentation
process.

\item Offer usable development environment (Essential). This task is also
dependent on the completion of the Kit Compiler (or at least a
consistent version of it). However, it is not a huge coding task.

\item Semantics (Optional). It would be interesting to try and characterise
the behaviour of the obligation system and develop a verification
semantics to capture the informal understanding which I have employed.

\item Syntactic equality (Optional). In the original project description,
there was the option to discard trivial proof obligations. Most trivial
cases can be matched simply using syntactic equality and I have simple
code to do this. However, straight ML equality is too strong and
virtually no obligations are discharged. So, a looser equality is
required. This entails adding equality functions to all the EML syntax
objects (and thus relies on a consistent Kit Compiler).

\item Case study (Optional). Running a reasonable case study through the
system and confirming the obligations generated should offer further
evidence for the correctness. A suitable example development may come
from an earlier project for coursework.

\item Initial ML signature (Optional). ML native functions should strictly
be specified and their behaviour formalised. Most proofs rely on
axioms (usually assumed) about their behaviour but it is difficult to
axiomatise behaviour of, in particular, inifinite range real number
functions in a finite system.

\end{itemize}

\section{Timetable}

Below is a proposed timetable for work to project completion. It is
unlikely that the boundaries between the phases will be rigid (in
particular, I am hoping to do some preliminary documentation work as a
background task from now). The timetable is given (hopefully)
pessimistically (if this is not a contradiction).

\begin{itemize}

\item August 3rd - 14th. Integrate with Kit Compiler to provide
coherent usable package.

\item August 15th - 20th. Run through case study and confirm/improve
usability of package.

\item August 21st - 27th. Axiom equality and (time dependent) first
hack at semantics.

\item August 28th - September 2nd. Revitalisation and buffer zone.

\item September 3rd - 28th. Report production.

\end{itemize}
