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