Formal Methods: Z CS 415, Software Engineering II Mark Ardis, Rose-Hulman Institute March 18, 2003 Outline Types of Formal Methods Introduction to Z Examples 2
Formal Methods Specification and verification methods Have formal (mathematical) semantics unambiguous facilitate proofs of correctness
In use since late 1970s more popular in Europe than US still only a niche market 3 Types of Formal Methods Model-theoretic
VDM, Algebraic ACT One, Larch , OBJ Concurrent processes
CCS, Z CSP, Petri Nets Finite State Machines Esterel,
Statecharts Hybrid LOTOS, SDL 4 Model-theoretic Methods
Vienna Development Method (VDM) invented at IBM Vienna lab in late 1970s used for compilers (Denmark, Germany) and for information processing (England) Z Invented
by Jean-Raymond Abrial (France) Developed by Programming Research Group (PRG) at Oxford Used at IBM Hursley in mid 1980s 5 Foundations of Z Model theoretic method abstract
model is constructed properties of the model are proven Set theory (and other discrete math) First order predicate calculus Schema calculus provides incrementality 6 Predicate Logic
Variables ranging over arbitrary sets Predicates: assertions about variables Operators: conjunction: A B disjunction: A B negation: A implication: A B
Quantifiers universal: x: T R(x) existential: x: T R(x) 7 Set Theory Membership: x S, x T Union: S T Intersection: S T
8 Functions and Relations element mapping: x y domain, range: dom(R), ran(R) overriding: R S partial function: x y 9
Sequences definition: <>, concatenation: length: #S functions: head(S) first element tail(S) all but the first element last(S) last element front(S) all but the last element
10 Schema Operators conjunction: S T disjunction: S T hiding: S \ (v1, , vn) hiding: S \ T overriding: S T
11 Names Variables input: name? output: name! postcondition: name'
Schema changes state: Name constant state: Name 12 Schemas Name declarations predicates
13 Birthday Book [Spivey 92] Example of use of schemas Describes a calendar with birthdates 14 BirthdayBook known: P NAME
birthday: NAME DATE known = dom birthday 15 Examples known = { Mark, Cheryl, Eric, Paul } birthday = { Mark
Cheryl July 9, Eric July 14, Paul April 30 April 7, } 16
AddBirthday BirthdayBook name? : NAME date? : DATE name? known birthday' = birthday {name? date?} 17
FindBirthday BirthdayBook name? : NAME date! : DATE name? known date! = birthday(name?) 18 Remind BirthdayBook today? : DATE
cards! : P NAME cards! = { n: known | birthday(n) = today? } 19 Initialization InitBirthday BirthdayBook known = 20
Deriving Properties known' = dom birthday' = dom ( birthday {name? date?} ) = dom birthday dom {name? date?} = dom birthday { name? } = known { name? }
21 Cartoon of the Day 22 Cartoon of the Day (cont.) 23 Symbol Table [Hayes 87] Describes a relation between symbols and
values Illustrates use of schema operators 24 Initial Definitions ST SYM st ST st0 VAL
25 Retrieve ST s? : SYM v! : VAL s? dom(st) v! = st(s?) 26
Declare ST s? : SYM v? : VAL st' = st { s? v? } 27 NotPresent ST
s? : SYM rep! : REPORT s? dom(st) rep! = "Symbol not present" 28 Success rep! : REPORT rep! = "OK" 29
Combining Schemas STRetrieve ( Retrieve Success) NotPresent STDeclare Declare Success 30 Overriding Definitions Introduce a new symbol table for each level of scope Need to override the previous definitions
of symbols: {s v} {s w} Need to introduce a distributed override operator for sequences of symbol tables 31 Block-Structured Symbol Tables BST seq ST
/ : seq ST ST / <> = / ( s < t > ) = (/ s ) t bst0 < > 32 BStart0 BST bst' = bst < st0 > BEnd0 BST
bst < > bst' = front( bst ) 33 Z Method 1. 2. 3. 4. 5. Introduce basic sets
Define an abstract state in terms of sets, functions, relations, sequences, etc. Specify the initial state Define pre- and post-conditions of operations State and prove theorems 34 References Ian Hayes (editor), Specification Case Studies, Prentice-Hall International, 1987, ISBN 0-13-826579-8.
J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall International, 1992, ISBN 0-13-978529-9. 35