National Science Library of Georgia

Image from Google Jackets

Formal specification and design / L.M.G. Feijs & H.B.M. Jonkers.

By: Contributor(s): Material type: TextTextSeries: Cambridge tracts in theoretical computer science ; 35.Publisher: Cambridge : Cambridge University Press, 1992Description: 1 online resource (xvi, 335 pages) : digital, PDF file(s)Content type:
  • text
Media type:
  • computer
Carrier type:
  • online resource
ISBN:
  • 9780511569777 (ebook)
Other title:
  • Formal Specification & Design
Subject(s): Additional physical formats: Print version: : No titleDDC classification:
  • 005.1/2 20
LOC classification:
  • QA76.76.D47 F44 1992
Online resources:
Contents:
3.7. Semantics of normal-form specifications. 3.8. Hidden names. 4. Implementing algebraic specifications. 4.2. Expressions. 4.3. Term interpretation of expressions. 4.4. Declarations. 4.5. Survey of assertions and expressions. 4.6. Algorithmic predicate definitions. 4.7. Algorithmic function definitions. 4.8. From inductive to algorithmic definitions. 4.9. Implementing an algebraic specification. 4.10. Example: implementation of sets -- II. State-based specification. 5. From algebras to states. 5.2. What is a state-based specification? 5.3. Procedure names and class signatures. 5.4. States as algebras. 5.5. Classes. 5.6. Introducing variables. 5.7. Procedure definitions. 5.8. Comparison with imperative programs. 5.9. From predicate logic to dynamic logic. 5.10. Classes and specifications. 6. Setting up state-based specifications. 6.1. Kinds of axioms.
8.7. Example: implementation of a line editor. 8.7.1. Specifying the system. 8.7.2. Documenting a building block. 8.7.3. Choosing a representation. 8.7.4. Adding display-oriented features. 8.7.5. Implementing the display-oriented features. 8.7.6. Translation to C. 8.7.7. Executing the program -- III. Advanced techniques. 9. Theoretical topics. 9.2. Undefinedness revisited. 9.3. Initial algebras. 9.4. Horn clauses. 9.5. Origin consistency. 9.6. Comparing two types of models. 9.7. The class concept revisited. 10. Additional language constructs. 10.2. Liberal scope rules. 10.3. Free definitions. 10.4. Parameterisation. 10.5. Abstraction schemes. 10.6. Application schemes. 10.7. Extending the normalization procedure. 10.8. More complex parameter restrictions. 10.9. Object creation and procedures with results. 10.10. Variable sort definitions. 10.11. Dependent definitions. 10.12. Example: specification of instances. 10.13. Unifying expressions and statements. 11. Towards large systems.
11.2. Graphical representation of modules. 11.3. Components and designs. 11.4. Applications. 11.5. Concluding remarks -- A Syntax. A.1 General. A.2 Concrete syntax. A.3 Tokens. A.4 Keywords. A.5 Comments. A.6 Grammar. A.7 Operator priorities and associativities. A.7.1 Operators in renamings and signatures. A.7.2 Operators in assertions and expressions -- B Standard library. B.1 Booleans. B.2 Natural numbers. B.3 Characters. B.4 Tuples. B.5 Finite sets. B.6 Finite bags. B.7 Finite sequences. B.8 Finite maps.
Summary: Formal specification is a method for precisely modelling computer-based systems that combines concepts from software engineering and mathematical logic. In this book the authors describe algebraic and state-based specification techniques from the unified view of the Common Object-oriented Language for Design, COLD, a wide-spectrum language in the tradition of VDM and Z. The kernel language is explained in detail, with many examples, including: set representation, a display device, an INGRES-like database system, and a line editor. Fundamental techniques such as initial algebra semantics, loose semantics, partial functions, hiding, sharing, predicate and dynamic logic, abstraction functions, representation of invariants and black-box correctness are also presented. More advanced ideas, for example Horn logic, and large systems are given in the final part. Appendices contain full details of the language's syntax and a specification library. Techniques for software development and design are emphasised throughout, so the book will be an excellent choice for courses in these areas.
Tags from this library: No tags from this library for this title. Log in to add tags.
No physical items for this record

Title from publisher's bibliographic system (viewed on 05 Oct 2015).

3.7. Semantics of normal-form specifications. 3.8. Hidden names. 4. Implementing algebraic specifications. 4.2. Expressions. 4.3. Term interpretation of expressions. 4.4. Declarations. 4.5. Survey of assertions and expressions. 4.6. Algorithmic predicate definitions. 4.7. Algorithmic function definitions. 4.8. From inductive to algorithmic definitions. 4.9. Implementing an algebraic specification. 4.10. Example: implementation of sets -- II. State-based specification. 5. From algebras to states. 5.2. What is a state-based specification? 5.3. Procedure names and class signatures. 5.4. States as algebras. 5.5. Classes. 5.6. Introducing variables. 5.7. Procedure definitions. 5.8. Comparison with imperative programs. 5.9. From predicate logic to dynamic logic. 5.10. Classes and specifications. 6. Setting up state-based specifications. 6.1. Kinds of axioms.

8.7. Example: implementation of a line editor. 8.7.1. Specifying the system. 8.7.2. Documenting a building block. 8.7.3. Choosing a representation. 8.7.4. Adding display-oriented features. 8.7.5. Implementing the display-oriented features. 8.7.6. Translation to C. 8.7.7. Executing the program -- III. Advanced techniques. 9. Theoretical topics. 9.2. Undefinedness revisited. 9.3. Initial algebras. 9.4. Horn clauses. 9.5. Origin consistency. 9.6. Comparing two types of models. 9.7. The class concept revisited. 10. Additional language constructs. 10.2. Liberal scope rules. 10.3. Free definitions. 10.4. Parameterisation. 10.5. Abstraction schemes. 10.6. Application schemes. 10.7. Extending the normalization procedure. 10.8. More complex parameter restrictions. 10.9. Object creation and procedures with results. 10.10. Variable sort definitions. 10.11. Dependent definitions. 10.12. Example: specification of instances. 10.13. Unifying expressions and statements. 11. Towards large systems.

11.2. Graphical representation of modules. 11.3. Components and designs. 11.4. Applications. 11.5. Concluding remarks -- A Syntax. A.1 General. A.2 Concrete syntax. A.3 Tokens. A.4 Keywords. A.5 Comments. A.6 Grammar. A.7 Operator priorities and associativities. A.7.1 Operators in renamings and signatures. A.7.2 Operators in assertions and expressions -- B Standard library. B.1 Booleans. B.2 Natural numbers. B.3 Characters. B.4 Tuples. B.5 Finite sets. B.6 Finite bags. B.7 Finite sequences. B.8 Finite maps.

Formal specification is a method for precisely modelling computer-based systems that combines concepts from software engineering and mathematical logic. In this book the authors describe algebraic and state-based specification techniques from the unified view of the Common Object-oriented Language for Design, COLD, a wide-spectrum language in the tradition of VDM and Z. The kernel language is explained in detail, with many examples, including: set representation, a display device, an INGRES-like database system, and a line editor. Fundamental techniques such as initial algebra semantics, loose semantics, partial functions, hiding, sharing, predicate and dynamic logic, abstraction functions, representation of invariants and black-box correctness are also presented. More advanced ideas, for example Horn logic, and large systems are given in the final part. Appendices contain full details of the language's syntax and a specification library. Techniques for software development and design are emphasised throughout, so the book will be an excellent choice for courses in these areas.

There are no comments on this title.

to post a comment.
Copyright © 2023 Sciencelib.ge All rights reserved.