Abstract
This thesis documents research that enables formal specifications, written in the specification language Z, to be turned into high level code in fewer steps than other refinement techniques and without the need for formal proof. This method helps to overcome one of the mam stumbling blocks for formal methods, which is the difficulty of creating software from the formal specification. In the main, previous methods have either concentrated on creating an animation or prototype of the specification using functional languages or on converting the abstract structures found in specification into the less abstract structures found in high level programming languages, via a series of lengthy proofs.The method presented in this thesis uses a different approach. Here, the target language is enriched with the abstract structures and operations available to the formal specification language. This is achieved by the construction of a series of reusable software components that model the main types and operations found in Z. The formal specification can then be translated into executable code by selecting the correct operations from the reusable components to implement each of the Z operations.
The research described in this thesis shows that the method is a viable one. as efficient executable code can be produced very quickly, without the need for formal proof, and with great confidence in its correctness. The components required to do this are available and have been written and constructed in such a way as to allow more complex components to be built from them.
| Date of Award | Aug 1998 |
|---|---|
| Original language | English |
| Supervisor | John Hayward (Supervisor) |