Project History

1996

The project was supported in 1996 by an ARC small grant. This work led to an initial version of wide-spectrum language that includes both specification and more traditional programming constructs. This language included general predicates, assumptions, sequential conjunction and procedures. A semantics for this language were developed, based on ok and effect functions, and a basic set of refinement rules were verified against these semantics. In an honours project, Robert Colvin developed prototype tool support for this initial version of the refinement calculus, based on the Ergo 4 theorem prover.

The project members for 1996 were Ian Hayes, Paul Strooper, Ray Nickson, and Robert Colvin.

1999

The project was supported in 1999 (and subsequently up until early 2002) by an Australian Research Council (ARC) Large Grant. David Hemer joined the project in August and Richard Hagen from October. In 1999 work continued on generalising the previous semantics by modelling commands as partial mappings from a set of bindings to a subset of the bindings. David worked on Isabelle-based tool support, and Richard on code generation from tool-generated output. Robert Colvin continued work on his PhD, in particular investigating the role of types in program refinement, and the concept was extended to relationships between variables (invariants).

2000

In 2000 work continued on devising and documenting the semantics of logic program refinement. This work generalises an earlier semantics by modelling commands as partial mappings from a set of bindings to a subset of the bindings. These semantics were used in the development of Marvin, a tool based on the Isabelle/HOL theorem prover, to support the refinement of logic programs. Associate Investigator Ray Nickson visited the SVRC in 2000 to work on the project.

The project members for 2000 were Ian Hayes, Paul Strooper, Ray Nickson, Robert Colvin, Richard Hagen and David Hemer.