• Produktbild: Mural: A Formal Development Support System
  • Produktbild: Mural: A Formal Development Support System

Mural: A Formal Development Support System

51,99 €

inkl. gesetzl. MwSt., Versandkostenfrei


Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

29.05.1991

Verlag

Springer Berlin

Seitenzahl

421

Maße (L/B/H)

24,2/17/2,4 cm

Gewicht

753 g

Auflage

Softcover reprint of the original 1st ed. 1991

Sprache

Englisch

ISBN

978-3-540-19651-8

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

29.05.1991

Verlag

Springer Berlin

Seitenzahl

421

Maße (L/B/H)

24,2/17/2,4 cm

Gewicht

753 g

Auflage

Softcover reprint of the original 1st ed. 1991

Sprache

Englisch

ISBN

978-3-540-19651-8

Herstelleradresse

Springer-Verlag KG
Sachsenplatz 4-6
1201 Wien
AT

Email: ProductSafety@springernature.com

Kundinnen und Kunden meinen

0 Bewertungen

Informationen zu Bewertungen

Zur Abgabe einer Bewertung ist eine Anmeldung im Konto notwendig. Die Authentizität der Bewertungen wird von uns nicht überprüft. Wir behalten uns vor, Bewertungstexte, die unseren Richtlinien widersprechen, entsprechend zu kürzen oder zu löschen.

Die Bewertungen sind nach Format, Anzahl Sterne und Datum sortiert.

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kund*innen durch Ihre Meinung

Kundinnen und Kunden meinen

0 Bewertungen filtern

  • Produktbild: Mural: A Formal Development Support System
  • Produktbild: 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.