|
" Formal specification : "
Nimal Nissanke.
| Document Type
|
:
|
BL
|
| Record Number
|
:
|
731833
|
| Doc. No
|
:
|
b551619
|
| Main Entry
|
:
|
Nimal Nissanke.
|
| Title & Author
|
:
|
Formal specification : : techniques and applications\ Nimal Nissanke.
|
| Publication Statement
|
:
|
New York: Springer, 1999
|
| Page. NO
|
:
|
xvii, 291 pages
|
| ISBN
|
:
|
1852330023
|
|
|
:
|
: 9781852330026
|
| Contents
|
:
|
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.3 Overloading, Genericity and Polymorphism.- 8.5 Abstract Data Types and Classes.- 8.6 Representation of Classes.- 8.7 Object Oriented Specification Languages.- 8.7.1 An Object Oriented Syntax in Z Style.- 8.8 Object Oriented Version of Sequences.- 8.9 Text Processing.- 8.9.1 A Character Set.- 8.9.2 Textual Objects.- 8.9.3 Text as Scripts.- 8.9.4 Text as Documents.- 8.9.5 Text as Dialogue.- 8.9.6 Text Windows.- Exercises.- 9. Specification of Safety.- 9.1 Introduction.- 9.2 Specification Framework.- 9.2.1 Changes in States as Time Histories.- 9.2.2 Representation of Equipments.- 9.2.3 A Classification of Safety Requirements.- 9.2.4 Specification of Safety Requirements.- 9.3 Description of System State and Behaviour.- 9.3.1 Tracks.- 9.3.2 Signals.- 9.3.3 Points.- 9.3.4 Subroutes.- 9.3.5 Routes.- 9.4 System Behaviour in the Presence of Failures.- 9.4.1 Behavioural Specification of Sensors.- 9.4.2 Behavioural Specification of the Controller.- 9.4.3 Behavioural Specification of Signals.- 9.4.4 Behavioural Specification of Points.- 9.4.5 Behavioural Specification of Tracks.- 9.5 Preventing and Averting Failures.- 9.5.1 Low to High Risk State Transitions.- 9.5.2 High to Low Risk State Transitions.- Concluding Remarks.- Exercises.- 10. An Overview of VDM.- 10.1 Standard Mathematical Notation.- 10.1.1 A General Comment.- 10.1.2 Logic.- 10.1.3 Types.- 10.1.4 Sets and Relations.- 10.1.5 Mathematical Functions.- 10.2 Specification of State Based Systems.- 10.2.1 Specification Structure.- 10.2.2 A Comparison with Z.- 10.3 Composite Objects.- 10.4 Musical Chairs - An Example.- 10.4.1 State Model.- 10.4.2 Initialization.- 10.4.3 Other Operations.- 10.4.4 Execution Order of Operations.- 10.4.5 VDM Specification of Musical Chairs.- 10.5 An Indexed Filing System - A Case Study.- 10.5.1 An Informal Description of Requirements.- 10.5.2 System Organization.- 10.5.3 Model of Individual Files.- 10.5.4 VDM Specification of Indexed Files.- 10.5.5 Model of the Module Interface.- 10.5.6 Model of the Filing System.- 10.5.7 VDM Specification of the Indexed Filing System.- Exercises.- 11. Algebraic Approach to Specification.- 11.1 Introduction.- 11.2 A Preliminary Comparison.- 11.2.1 Model Oriented Approach.- 11.2.2 Algebraic Approach.- 11.3 Algebraic Notions.- 11.3.1 Some Basic Algebras.- 11.3.2 Homogeneous Algebras.- 11.3.3 Heterogeneous Algebras.- 11.3.4 Type Algebras.- 11.4 Many-sorted Algebra.- 11.4.1 Signatures.- 11.4.2 Signature Associated Algebra.- 11.4.3 Subalgebras.- 11.5 Homomorphisms.- 11.5.1 Characterisation of Homomorphism.- 11.6 Term Algebras.- 11.6.1 Well Formed Terms.- 11.6.2 Natural Numbers as a Homogeneous Data Type.- 11.6.3 Heterogeneous (Many-Sorted) Abstract Data Types.- 11.7 Equations.- 11.7.1 Variables.- 11.7.2 Algebras and Equations.- 11.7.3 Other Related Terminology.- 11.7.4 Equational Deduction.- 11.8 Initial Algebras.- 11.8.1 The Motivation for Initial Algebras.- 11.8.2 The Definition of Initiality.- 11.9 Terminal Algebras.- 11.9.1 The Motivation for Terminal Algebras.- 11.9.2 Reasoning About Inequalities.- 11.10Bibliographical Notes.- 12. Algebraic Specification in CLEAR.- 12.1 Data Types and Systems.- 12.2 Views of Specifications.- 12.3 An Introduction to CLEAR.- 12.3.1 Sorts, Operators, Terms and Equations.- 12.3.2 Simple Theories.- 12.3.3 Complex Theories.- 12.3.4 Parameterised Theories.- 12.3.5 Meta Theories.- 12.3.6 Base Theories.- 12.3.7 Specifications.- 12.4 A Case Study: A Filing System.- 12.4.1 Some Basic Specifications.- 12.4.2 A General Specification for Various Kinds of Object.- 12.4.3 Maps.- 12.4.4 Sequences.- 12.4.5 Indexed Files.- 12.4.6 Sequential Files.- 12.4.7 File System.- 12.5 Bibliographical Notes.- Exercises.- A. Exercises on Reading Formal Specifications.- A.1 Exercise - A Simple Text Editor.- A.2 Let's Play A Game of Cards.- A.3 Unix Filing System.- B.
|
|
|
:
|
Exercises on Writing Formal Specifications.- B.1 A Catalogue Shop.- B.2 Know Your Place if You Succeed in Politics!.- B.3 Traffic Lights.- B.4 A Vending Machine.- B.5 A Bank.- B.6 A Flight Reservation Service for an Airline.- B.7 A Hospital Register.- C. The Mathematical Notation.- References.
|
| Subject
|
:
|
Application software -- Development.
|
| Subject
|
:
|
Formal methods (Computer science)
|
| LC Classification
|
:
|
QA76.9.F67N563 1999
|
| Added Entry
|
:
|
Nimal Nissanke
|
| |