Formal methods 4 - Z notation

My course of Formal Methods at Santa Clara University, Winter 2014.

1. Formal Methods in
Software
Lecture 4. Z Notation
Vlad Patryshev
SCU
2014
you may need Chrome browser to view these slides

2. Z Notation, a Specification Language
●Vaguely based on typed version of Zermelo-Fraenkel set theory
●Uses set-theoretic notation for algorithm description
●Software tools exist(ed) that could, arguably, verify algorithms
●Related to computational logic
●Partially replaced these days by Coq and Agda
●ISO standard: ISO/IEC 13568:2002
●WSDL definition uses it
●Lives in an ideal world, not very good for programming with effects
●But is related to Agda

3. The Logic of Z
●Propositional logic
○predicates; true/false
○connectives: a∧b, a∨b,¬a, a⇒b, a⇔b
●Quantifiers
○∀x • q
○∃x • q
○∃
1
x • q (“exists unique”)
●Many laws (but nothing unusual)

4. Z has types and constraints
a:T - a is of type T
q a - a satisfies a constraint (a predicate) q

E.g.



a,b: Human
x: Dog
likes(a,x)
likes(b,x)
loves(x,a)
loves(x,b)
Signature
Predicates (constraints)

5. Z uses typed sets
●∅[T] - empty set of elements of type T
●{Peter, Paul, James} - a set of people; elements must be of the same type
●order does not matter; repetitions make no sense
●x∈S - x is an element of S e.g. William ∉ {Jonathan, Jane, Alice, Emma}
●P∪Q - union
●P∩Q - intersection
●P\Q - complement ({x∈P|x∉Q})
●P ⊆ Q - P is a subset of Q (P∩Q=P)
●P
-
- complement of P, all members of type that do not belong to P (P
-
=T\P)
E.g. T
-
=∅[T] and ∅[T]
-
=T
●∪{A,B,C,...} = A∪B∪C∪…
●∩{A,B,C,...} = A∩B∩C∩…

6. Set Comprehension
{x∈T|P(x)} - a set of all such x that P(x) is true

Properties:
●{x:T |p}∩{x:T |q}={x:T |p ∧q}
●{x:T |p}∪{x:T |q}={x:T |p∨q}
●{x:T |p}− ={x:T |¬p}
●{x:T |p}⊆{x:T |q} ≡ p⇒q
●{x:T |p}={x:T |q} ≡ p ⇔q
●∅[T]={x:T |false}
●T={x:T |true}

7. Cartesian Product
If T and U are types,
T×U is the type of pairs (t,u), where t:T, u:U

If P and Q are sets, P×Q = {p:T; q:U|p∈P∧q∈Q • (p,q)}
(meaning, take ps from P, qs from Q, produce all pairs (p,q))

8. Powerset
X∈ℙS ≡ X⊆S
E.g.
ℙ∅ = {∅}; ℙ{a} = {∅,{a}}
Finite subsets of S: FS
ℙ
1
S = {X∈ℙS | X!=∅}
F
1
S = {X∈FS | X!=∅}

9. Binary Relations
R⊆P×Q
Notation: given a relation R, pRq means (p,q)∈R
Alternative notation for pairs (p,q): p↦q
E.g. authors = {Bjarne ↦ Cpp, Guido ↦ Python, Martin ↦
Scala}

Set of all relations T ↔ U == ℙ(T × U)
E.g. authors ∈ Humans ↔ Languages

10. Domain and Range
R ∈ T ↔ U
dom R = {x:T |(∃y:U•(x,y)∈R)} - not a very good idea, actually
ran R = {y:U |(∃x:T•(x,y)∈R)} - an even worse idea

E.g.
dom authors = {Bjarne, Guido, Martin}
ran authors = {Cpp, Python, Scala}

11. Inverse Relation
Every relation has an inverse
R
∼
= {y:U;x:T|(x,y)∈R}

E.g. authors = {Bjarne↦Cpp, Guido↦Python, Martin↦Scala}
authors
~
= {Cpp↦Bjarne, Python↦Guido, Scala↦Martin}

Obviously,
●ran(R
∼
) = dom R
●dom(R
∼
) = ran R
●(R
∼
)
∼
= R

12. Functions are Relations
●Partial Function f: A B ≡
∀x:A ∀y
1
,y
2
:B (x,y
1
)∈f∧(x,y
2
)∈f⇒y
1
=y
2

●Total function f: A→B ≡ f is p.f. and
∀x:A ∃y:B (x,y)∈f
●Injection f: A↣B ≡ f is function, and
∀x
1
,x
2
:A (x
1
,y)∈f∧(x
2
,y)∈f⇒x
1
=x
2

●Surjection f: A↠B: f is function, and
∀y:B ∃x:A (x,y)∈f
●Partial injection, partial surjection
●Finite partial function, A B

13. ●Identity id A = {(x,x):T×T|x ∈A}
●RTL Composition Q∘R = {(z,x):T×V|∃y:U•(y,x)∈R∧(z,y)∈Q}
●Domain restriction A◁R = {(x,y):T×U|(x,y) ∈R∧x∈A}
●Domain anti-restriction AR = {(x,y):T×U|(x,y) ∈R∧x∉A}
●Range restriction A▷R = {(x,y):T×U|(x,y) ∈R∧y∈A}
●Range anti-restriction AR = {(x,y):T×U|(x,y) ∈R∧y∉A}
●Image R(|A|) = {y:U|∃x:T•(x,y)∈R∧x∈A
●Inverse R
~
●Iteration iter n R = R∘(iter (n-1) R); iter 0 R = id
●Overriding Q⨁R = (dom R Q) ∪ R
Operations on Relations

14. Numbers
●ℤ - all integers
●ℕ = {x∈ℤ|x≥0}
●_+_, _-_, _*_, _div_, _mod_, -_
●_≥_, _>_, _≤_, _<_
●max(<nonempty set>), min

15. Axiomatic Description
●new operator



●new data with constraint









abs : Z → Z
∀n:Z•
n ≤ 0 ⇒ abs n = −n ∧ n ≥ 0 ⇒ abs n = n
n:ℕ
n<10

16. Iteration etc
●Introduce succ=={0↦1,1↦2,...}; pred==succ
~

●succ = ℕ◁(_+1)

●R
n
=R∘R∘...∘R
e.g. succ
n
= ℕ◁(_+n)
●Number range a..b={n:ℕ|a≤n≤b}
●Cardinality of set S ∈ F T , #S
(For a set to be ‘finite’, it must be in bijection with 1..n for some n.)

17. Introducing New Types
●Just by naming, [A]
●data type (like enum): Friends ::= Peter|John|James
●recursively, e.g. ℕ ::= zero | succ⟨⟨ℕ⟩⟩

18. Sequences
seq T =={s:ℕT |∃n:ℕ • dom s = 1..n}

●⟨⟩ - empty sequence
●Nonempty sequence seq
1
T == seq T \ {⟨⟩}
●Injective sequence iseq T == {f: seq T| injective f}
●⟨’a’,’b’,’c’⟩
●concatenation: ⟨’a’,’b’,’c’⟩◠⟨’d’,’e’,’f’⟩
●prefix ⟨’a’,’b’⟩ ⊆ ⟨’a’,’b’,’c’⟩
●head s = s(1); last s = s(#s); tail s; front s
●rev ⟨⟩ = ⟨⟩, rev ⟨x⟩ = ⟨x⟩, rev(s◠t) = rev(t)◠rev(s)

19. Schemas
Example:




alternatively,
Book≘[author:People;title:seq CHAR; readership: ℙ People;rating:0..10 |
readership = dom rating]
author:People
title: seq CHAR
readership: ℙ People
rating: ↠ 0..10
readership = dom
rating
Book

20. State Machine: Operational Schema
Operation ≘ [
x
1
:S
1
;...;x
n
:S
n
; // current state
x
1
′:S
1
;...;x
n
′:S
n
; // new state
i
1
?:T
1
;...;i
m
?:T
m
; // input
o
1
!:U
1
;...;o
p
!:U
p
// output
|
Pre(i
1
?,...,i
m
?,x
1
,...,x
n
); // preconditions
Inv(x
1
,...,x
n
); // invariants
 Inv(x
1
′,...,x
n
′); // invariants
Op(i
1
?,...,i
m
?,x
1
,...,x
n
,x
1
′ ,...,x
n
′ ,o
1
!,...,o
p
!) // step function
]

21. Example of Operational Schema
AddBirthday ≘ [
known : ℙ NAME;
birthday : NAME DATE
known′ : ℙ NAME;
birthday? : NAME DATE
name? : NAME;
date? : DATE;
|
name? ∉ known;
known = dom birthday;
known′ = dom birthday′;
birthday′ = birthday ∪ {name? ↦ date?}
]

22. Δ: Operational Schemas Reuse
StateSpace ≘ [ x
1
:S
1
;...;x
n
:S
n
| Inv(x
1
,...,x
n
) ]

Operation ≘ [
Δ StateSpace; // encapsulates changing state
i
1
?:T
1
;...;i
m
?:T
m
; // input
o
1
!:U
1
;...;o
p
!:U
p
// output
|
Pre(i
1
?,...,i
m
?,x
1
,...,x
n
); // preconditions
Op(i
1
?,...,i
m
?,x
1
,...,x
n
,x
1
′ ,...,x
n
′ ,o
1
!,...,o
p
!) // step function
]

23. Example of Δ inclusion
AddBirthday ≘ [
Δ BirthdayBook;
name? : NAME;
date? : DATE;
|
name? ∉ known;
birthday′ = birthday ∪ {name? ↦ date?}
]

24. Operations that don’t change State
Operation ≘ [
x
1
:S
1
;...;x
n
:S
n
; // current state
x
1
′:S
1
;...;x
n
′:S
n
; // new state
i
1
?:T
1
;...;i
m
?:T
m
; // input
o
1
!:U
1
;...;o
p
!:U
p
// output
|
Pre(i
1
?,...,i
m
?,x
1
,...,x
n
); // preconditions
Inv(x
1
,...,x
n
); // invariants
 Inv(x
1
′,...,x
n
′ ); // invariants
(x
1
’=x
1
∧x
2
’=x
2
∧...∧x
n
’=x
n
); // state does not change
Op(i
1
?,...,i
m
?,x
1
,...,x
n
,x
1
′ ,...,x
n
′ ,o
1
!,...,o
p
!) // step function
]

25. Ξ: Operational Schemas Reuse
Greek letter Ξ, pronounced as /ˈzaɪ/ or /ˈksaɪ/

Operation ≘ [
Ξ StateSpace; // encapsulates unchanging state
i
1
?:T
1
;...;i
m
?:T
m
; // input
o
1
!:U
1
;...;o
p
!:U
p
// output
|
Pre(i
1
?,...,i
m
?,x
1
,...,x
n
); // preconditions
Op(i
1
?,...,i
m
?,x
1
,...,x
n
,x
1
′ ,...,x
n
′ ,o
1
!,...,o
p
!) // step function
]

26. Example of Ξ inclusion
FindBirthday ≘ [
Ξ BirthdayBook;
name? : NAME;
date! : DATE;
|
name? ∈ known;
date! = birthday(name?)
]

27. And more...
●Can compose schema states
●Can connect schemas (output to input)
●Can include schemas

28. WSDL
http://www.w3.org/TR/wsdl20/wsdl20-z.html

ServiceComponents ≘ [ ComponentModel1; serviceComps : ℙ Service; endpointComps : ℙ Endpoint;|
serviceComps = { x : Service |service(x) ∈components }
endpointComps = { x : Endpoint | endpoint(x) ∈components }
]

29. References
http://images4.wikia.nocookie.net/formalmethods/images/4/4e/Zbook.pdf
ISO/IEC 13568:2002
W3C WSDL standard
Wikipedia