000 04939nam a22004218i 4500
001 CR9780511569777
003 UkCbUP
005 20200124160238.0
006 m|||||o||d||||||||
007 cr||||||||||||
008 090520s1992||||enk o ||1 0|eng|d
020 _a9780511569777 (ebook)
020 _z9780521434577 (hardback)
020 _z9780521435925 (paperback)
040 _aUkCbUP
_beng
_erda
_cUkCbUP
050 0 0 _aQA76.76.D47
_bF44 1992
082 0 0 _a005.1/2
_220
100 1 _aFeijs, L. M. G.
_q(Loe M. G.),
_eauthor.
245 1 0 _aFormal specification and design /
_cL.M.G. Feijs & H.B.M. Jonkers.
246 3 _aFormal Specification & Design
264 1 _aCambridge :
_bCambridge University Press,
_c1992.
300 _a1 online resource (xvi, 335 pages) :
_bdigital, PDF file(s).
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
490 1 _aCambridge tracts in theoretical computer science ;
_v35
500 _aTitle from publisher's bibliographic system (viewed on 05 Oct 2015).
505 0 _a3.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.
505 0 _a8.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.
505 0 _a11.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.
520 _aFormal 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.
650 0 _aComputer software
_xDevelopment.
650 0 _aObject-oriented programming (Computer science)
700 1 _aJonkers, H. B. M.,
_eauthor.
776 0 8 _iPrint version:
_z9780521434577
830 0 _aCambridge tracts in theoretical computer science ;
_v35.
856 4 0 _uhttps://doi.org/10.1017/CBO9780511569777
999 _c518251
_d518249