Formal Specification Using Z: A Modelling Approach
Formal Specification Using Z: A Modelling Approach is designed to provide a practical introduction to formal specification, explaining use of mathematically based techniques for specifying software systems in the formal specification language, Z. Of particular note is the text's concentration on the process of developing a specification and the clear distinction made between the process of constructing a mathematical model and the translation of that model into formal notation. The process of developing the specification is explained through the exploration of alternative mathematical models and the book emphasizes equally both model building and the use of a formal notation, in this case Z. Divided into four parts, Formal Specification Using Z begins by introducing the need for formal specification and discusses the general issue of modelling. Part two presents a selection of the basic mathematical tools and applies these to a number of modelling examples. Extended examples are presented in the third part of the book whilst part four places formal specification in the context of formal methods. Formal Specification Using Z: A Modelling Approach is ideal for computer science and software engineering students studying a first course in formal specification. It will also be of value to software development professionals.
What people are saying - Write a review
We haven't found any reviews in the usual places.
A First Example of Modelling and Speciﬁcation in Z
10 other sections not shown
after-state before-state blocks scene bottaci carParkCapacity Chapter class number coins components consider construct copier customsQueue database declaration deﬁned deﬁnition denote describe domain ECarPark elements empty empty set Exercise explicitly expression Figure ﬁnd ﬁrst ﬁsh ﬂoor formal speciﬁcation given set hire identiﬁed illustrated inﬁnite injective function input integers invariant item of equipment language maplet mathematical models means modula2 module notation number of copies number of ordinary onHire onTopOf ordinary customer ordinaryCars output pair paper partial function pass holder passenger passesIn passesInUse passport queue permits portfolio possible precondition predicate prerequisites print operation prolog quantiﬁer refund registered relation Relational composition REPORT represent requiredCopies satisﬁes scaling ratio schema sequence set of passes set union shareQues SmallCompany space specify stack state-based model statement subcase property subset success teachesProgramming toOrder total function transitive closure true truth table unary relation variable yogurt