mural: A Formal Development Support System

1General introduction.- 1.1 Formal methods.- 1.2 VDM development.- 1.3 The IPSE 2.5 project.- 1.4 Proof assistant requirements.- 2 Introduction to mural.- 2.1 General introduction.- 2.2 The proof assistant.- 2.3 The VDM support tool.- 2.4 Reasoning about developments.- 3 Instantiation.- 3.1 Symbolic logic in mural.- 3.2 Classical first order predicate calculus.- 3.3 Some common data types.- 3.4 More complicated formulations.- 3.5 The theory of VDM.- 3.6 Some other logics.- 4 Foundation.- 4.1 Preamble.- 4.2 Syntax.- 4.3 Natural Deduction rules.- 4.4 Rule Schemas and instantiation.- 4.5 The mural store.- 4.6 Syntactic contexts and well-formedness.- 4.7 Proofs.- 4.8 Morphisms.- 4.9 Pattern matching.- 4.10 Reading the full specification.- 4.11 Limitations of the mural approach.- 5 The tactic language.- 5.1 Mechanising proof in mural.- 5.2 The language.- 5.3 The implementation of tactics.- 5.4 Examples.- 6 Implementing the mural proof assistant.- 6.1 The process of implementation.- 6.2 The implementation.- 6.3 Lessons learnt and advice to the young.- 6.4 The future.- 6.5 The final word.- 7 Supporting formal software development.- 7.1 Abstract specification.- 7.2 Relating specifications.- 7.3 Support for reasoning about formal developments.- 8 The mural VDM Support Tool.- 8.1 Specifying VDM developments in VDM.- 8.2 Theories from specifications.- 8.3 Scope for growth.- 9 Foundations of specification animation.- 9.1 Approaches to animation.- 9.2 Denotational semantics of symbolic execution.- 9.3 Operational semantics of symbolic execution.- 9.4 Theories to support symbolic execution.- 9.5 Conclusions.- 10 Case Studies.- 10.1 Specifications in VDM.- 10.2 Transformation of VDM into mural -theories.- 10.3 A watchdog for a reactor system.- 10.4 An algorithm for topological sorting.- 10.5 Theories for VDM in mural.- 11 Conclusions.- 11.1 Experimental use of mural.- 11.2 Detailed observations.- 11.3 Further developments.- 11.4 Summary.- Appendices.- A Summary of VDM Notation.- B Glossary of terms.- C The Specification of the Proof Assistant.- C.1 The Raw Syntax.- C.2 Subterm Access and Editing.- C.3 Sequents and Rules.- C.4 Instantiation and Pattern-matching.- C.5 Signatures.- C.6 Theories.- C.7 Morphisms and Theory Morphisms.- C.8 Proofs.- C.9 The Store.- D The specification of the animation tool.- D.1 Data structure and some auxiliary functions.- D.2 Operations.- E The Theorem Prover's House.