Software EngineeringJump Over Left Menu
MURAL - An Interactive Proof Assistant
One reason often given for the slow adoption of formal methods is the lack of tools supporting the processes involved. MURAL, originally developed by Manchester University and RAL, was designed to assist with the theorem proving tasks arising in software engineering applications. Considerable emphasis was placed upon the design of the user interface, enabling users to maintain their intuition of the problem domain and guide the proof in the right direction, whilst the faultless symbolic manipulation of the machine maintained the integrity of the proof. An exploratory style of working was encouraged with the intention of assisting the proof discovery process rather than merely serving to check proofs previously worked out on paper. Proofs can be constructed by working forwards from the hypotheses, backwards from the conclusion, or from new lines added directly to the middle of the proof. Lines of reasoning can be temporarily abandoned whilst alternative approaches are attempted or lemmas conjectured and proved on the fly.
An instantiation of the proof assistant was developed for the Vienna Development Method (VOM) providing support for the creation of specifications and reifications between them, and also for the construction of the theories that provided the context in which proof obligations could be meaningfully discharged. As part of RAL's contribution to the original MURAL development project, a prototype VDM Support Tool was produced to maintain a store of VDM developments and generate MURAL theories from them (see figure below). The tool supported a small subset of the VDM specification language, and a limited form of reification initially, this was later extended to support a richer reification model which improved the theory generation.
A typical MURAL interactive session.
Full Size Image
MURAL attracted a great deal of interest from both the academic and industrial communities. Many indicated a desire to use it in the teaching of formal methods, logic and proof. Alvey supported the distribution of MURAL to the academic community and the improvements to the basic system and its user documentation.