mural: A Formal Development Support System

Häftad, Engelska, 1991

Av C.B. Jones, K.D. Jones, Peter Lindsay, R.D. Moore, C. B. Jones, K. D. Jones, R. D. Moore

729 kr

Beställningsvara. Skickas inom 10-15 vardagar

Fri frakt för medlemmar vid köp för minst 249 kr.

The MURAL project (a joint Alvey-funded project between Manchester University and Rutherford Appleton Laboratories) has developed a software support system to help the user of formal methods. MURAL has created a user-friendly software environment (with extensive use of windows) that makes best use of human talents to produce well-designed computer systems. This book describes the requirements, concepts and realization of the MURAL system. The contributors present the results of this substantial research project, from the basic theoretical level to its effective implementation.

Produktinformation

Utgivningsdatum1991-05-29
Mått170 x 242 x 24 mm
Vikt748 g
FormatHäftad
SpråkEngelska
Antal sidor421
FörlagSpringer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN9783540196518

Tillhör följande kategorier

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.