Formal methods enable computer architecture and software design to be mathematically proved correct before they are implemented. The complexity and time-consuming nature of such proofs have limited the applications of formal methods in the main to defence and safety-critical applications. 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 computer systems that are proved to be correctly designed. Professor Cliff Jones is internationally known as the developer of the VDM system of formal notation (Vienna Development Method). This book describes the requirements, concepts, and realisation of the mural system. The authors present systematically and completely the results of this substantial research project, from the basic theoretical level to its effective implementation. The book will be of equal interest to academics working on formal methods at research level (and perhaps to graduate research students), and to practitioners and software engineers who are using - or who will have to use for defence contracts, etc. - formal methods.

Contenuti

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.

Le informazioni nella sezione "Su questo libro" possono far riferimento a edizioni diverse di questo titolo.

Descrizione libreria

SuperBookDeals.com is your top source for finding new books at the absolute lowest prices, guaranteed ! We offer big discounts - everyday - on millions of titles in virtually any category, from Architecture to Zoology -- and everything in between. Discover great deals and super-savings, on professional books, text book titles, the newest computer guides, or your favorite fiction authors. You'll find it all - at HUGE SAVINGS - at SuperBookDeals. Browse through our complete online product catalog today. Serving customers around the world for years, we help thousands find just the books they're looking for -- at incredibly low, bargain prices.

Visita la pagina della libreria

Informazioni sull?azienda del venditore

Expert Trading Limited
9220 Rumsey Road, Suite 101, Columbia, MD, 21045, U.S.A.

Condizioni di vendita e spedizione

Condizioni di vendita

Company Name: GreatBookPrices
Legal Entity: Expert Trading, LLC
Address: 6310 Stevens Forest, suite 200, Columbia MD 21046
Email address: CustomerService@SuperBookDeals.com
Phone number: 410-964-0026
consumer complaints can be addressed to address above
Registration #: 52-1713923
Authorized representative: Danielle Hainsey

Diritto di recesso

Condizioni di spedizione

Our warehouses across the globe are fully operational without substantial delays. We are working hard and continue to overcome the daily challenges presented by COVID-19. We appreciate your understanding.

Internal processing of your order will take about 1-2 business days. Please allow an additional 4-14 business days for Media Mail delivery. We have multiple ship-from locations - MD,IL,NJ,UK,IN,NV,TN & GA

Tariffe di spedizione da U.S.A. a Italia

Tariffe di spedizione da U.S.A. a Italia
Quantit� dell?ordine	Da 21 a 36 giorni lavorativi	Da 21 a 36 giorni lavorativi
Primo articolo	EUR 17.03	EUR 17.03

I tempi di consegna sono stabiliti dai venditori e variano in base al corriere e al paese. Gli ordini che devono attraversare una dogana possono subire ritardi e spetta agli acquirenti pagare eventuali tariffe o dazi associati. I venditori possono contattarti in merito ad addebiti aggiuntivi dovuti a eventuali maggiorazioni dei costi di spedizione dei tuoi articoli.