상세정보

Formal Specification provides the reader with a practical and versatile approach to constructing program specifications. It includes both model-based (Z/VDM) and algebraic (CLEAR) paradigms of specification and emphasizes the range of languages and approaches available. Its main advantage over other specification books is that is offers an unrivaled breadth of coverage of the area, encompassing all the recent important advances.

Formal Specification is a textbook for 2nd/3rd year undergraduate and postgraduate courses in Formal Methods which offers a practical and versatile approach to constructing specifications. It covers both model-based and algebraic approaches and emphasises the range of languages and approaches which are available. Mathematical principles are explained using examples from everyday life (like card games), in order to "demystify" them and make them more comprehensible. It includes: unrivalled coverage of the topic including all important, recent advances lots of exercises with model answers case studies to guide students through the main principles margin notes to identify key points. Readers of this book do not have to be fully competent in formal specification - it is written to be accessible to any student who wants to learn about the topic.

정보제공 :

1. Introduction.- 1.1 Specification and Correctness.- 1.2 Specification as a Contract.- 1.3 Specification as a Design Aid.- 1.4 Specification as a Human Endeavour.- 1.5 Specification as Abstraction.- 1.6 Modularity in Specifications.- 1.7 Benefits Beyond Precision.- 1.8 Formal Specification as an Emerging Technology.- 1.9 Specification Techniques.- 2. Schema Language.- 2.1 Introduction.- 2.2 Type Definitions in Z.- 2.2.1 Generic Types.- 2.2.2 Free (Enumerated) Types.- 2.2.3 Types Defined by Schemas.- 2.3 Mathematical Definitions in Z.- 2.3.1 Schema.- 2.3.2 Axiomatic Definitions.- 2.3.3 Generic Definitions.- 2.4 Presentation of Schemas.- 2.5 Schema Manipulation.- 2.5.1 Schema Extension.- 2.5.2 Merging Schemas.- 2.5.3 Schema Negation.- 2.6 Significance of Schemas.- 2.6.1 Schemas Instead of Declarations.- 2.6.2 Schemas and Mathematical Relations.- 2.6.3 Bindings.- 2.6.4 Schemas as Sets.- 2.6.5 Schemas as Types.- 2.6.6 In Lambda Notation.- 2.6.7 Schemas in Predicate Logic Formulae.- 2.7 Some Naming Conventions.- 2.7.1 Schema Decoration.- 2.7.2 Explicit Renaming of Components.- 2.7.3 Dot Notation.- 2.8 Hiding and Projection of Components.- 2.9 Notation for Specification of Systems.- 2.9.1 General.- 2.9.2 Types of Operations.- 2.9.3 Naming Conventions.- 2.9.4 Some Common Abbreviations.- 2.10 Schema Composition.- 2.11 Pre and Post Conditions.- 2.12 Promotion.- Exercises.- 3. An Approach to Specification.- 3.1 Introduction.- 3.2 An Initial Understanding.- 3.2.1 Identification of the Objects of Discourse and Operations.- 3.3 Abstraction and Modularisation.- 3.3.1 Abstraction.- 3.3.2 Modularisation.- 3.4 Flight Journey.- 3.5 Flight Accommodation.- 3.6 Definition of Flight.- 3.6.1 Definition of Flight State.- 3.6.2 Initialisation of Flight State.- 3.7 Operations on Flight.- 3.7.1 Passenger Details.- 3.7.2 An Auxiliary Definition.- 3.7.3 Messages.- 3.7.4 Operation of Booking a Seat.- 3.7.5 Operation of Cancelling a Booking.- 3.7.6 Query Operation on Seat Availability.- 3.8 An Airline.- 3.8.1 Abstract Representation.- 3.8.2 Initialisation.- 3.8.3 Shared Auxiliary Specifications.- 3.8.4 Airline Operations.- Concluding Remarks.- Exercises.- 4. Specification for Fun.- 4.1 Games as Systems.- 4.2 Musical Chairs.- 4.2.1 The Problem Description.- 4.2.2 A Mathematical Description.- 4.3 Snakes and Ladders.- 4.3.1 The Problem Description.- 4.3.2 The Preliminaries.- 4.3.3 Some Notes on Decomposition.- 4.3.4 A Simple Game.- 4.3.5 The Full Game.- 4.3.6 An Illustration.- Exercises.- 5. A Specification for Clocks.- 5.1 Representation of Time.- 5.1.1 Notions of Time.- 5.1.2 Real Time.- 5.1.3 Points and Intervals of Time.- 5.1.4 Clock Time.- 5.2 A Mathematical Definition of Clocks.- 5.2.1 Clock Mechanism.- 5.3 Clock Utilities.- 5.3.1 Idealised Clock with Utilities.- 5.4 Operations and Transitions.- 5.4.1 Initialisation and Resetting.- 5.4.2 Clock Advancement.- 5.4.3 The Functioning of the Alarm.- 5.5 Intervals in Real Time.- Concluding Remarks.- Exercises.- 6. Reasoning About Specifications.- 6.1 Introduction.- 6.2 Kinds of Internal Consistency.- 6.3 Consistency of the General State.- 6.4 Initialisation Consistency.- 6.5 Consistency of Operations.- 6.5.1 Forms of Operation Inconsistency.- 6.5.2 Proof of Operational Aspects.- 6.5.3 Proofs Obligatory on Specification Grounds.- 6.5.4 An Illustration.- Exercises.- 7. Specification of a Network Protocol.- 7.1 Introduction.- 7.2 OSI Reference Model.- 7.3 Some Preliminaries.- 7.4 Application Layer.- 7.5 Presentation Layer.- 7.5.1 Refinement of the Data Type Message.- 7.5.2 Proofs on Verification.- 7.6 Session Layer.- 7.7 Transport Layer.- 7.8 Selected Proofs.- 7.8.1 Proof of Reflexivity.- 7.8.2 Proof of Symmetry.- 7.8.3 Proof of Transitivity.- 7.9 Bibliographical Notes.- Exercises.- 8. Object Oriented Specification.- 8.1 Object Orientation in the Narrow Sense.- 8.2 Object Orientation in the Wider Sense.- 8.3 What are Objects?.- 8.4 Some Object Oriented Concepts.- 8.4.1 Software Reuse.- 8.4.2 Inheritance.- 8.4

정보제공 :