Formal Specification of Software

The Z Specification Language

Bernhard Beckert

U NIVERSITÄT KOBLENZ -L ANDAU

B. Beckert: Formal Specification of Software – p.1

The Z Specification Language

Based on

Typed first-order predicate logic

Zermelo-Fraenkel set theory
Rich notation

B. Beckert: Formal Specification of Software – p.2

The Z Specification Language

Based on

Typed first-order predicate logic

Zermelo-Fraenkel set theory
Rich notation

Invented/developed by
J.-R. Abrial, Oxford University Computing Laboratory

International standard
ISO/IEC JTC1/SC22

B. Beckert: Formal Specification of Software – p.2

The Z Specification Language

Tools

LATEX style
Type checker
Z/Eves deduction system

But
No tools for simulation/execution/testing

B. Beckert: Formal Specification of Software – p.3

Built-in Operators

Logical operators

¬ negation
∧ conjunction
∨ disjunction
⇒ implication (note: not →)
⇔ equivalence (note: not ↔)

Equality

= equality

On all types (but not predicates)

B. Beckert: Formal Specification of Software – p.4

Built-in Operators

Quantification

Q x1 : S 1 ; . . . ; x n : S n | p • q

where Q is one of ∀ ∃ ∃1

Meaning

∀ x1 : S1 ; . . . ; xn : Sn (p ⇒ q) resp.
∃ x1 : S1 ; . . . ; xn : Sn (p ∧ q)

Abbreviation

∀ x : T • q for ∀ x : T | true • q

B. Beckert: Formal Specification of Software – p.5

Notation for Sets

Enumeration

{e1 , . . . , en }

The set of type-compatible elements e1 , . . . , en

Example

{3, 5, 8, 4}

B. Beckert: Formal Specification of Software – p.6

Notation for Sets

Set comprehension
{x : T | pred(x) • expr(x)}

The set of all elements that result from evaluating expr(x)

for all x of type T for which pred(x) holds

Example

{x : Z | prime(x) • x ∗ x}

The set of all squares of prime numbers

B. Beckert: Formal Specification of Software – p.7

Notation for Sets

Abbreviation
{x : T | pred(x)} for {x : T | pred(x) • x}

Example

N = {x : Z | x ≥ 0}

The empty set

∅ = {x : T | false}

Note:
∅ = ∅[T] is typed

B. Beckert: Formal Specification of Software – p.8

Set Operations

∈ element-of relation

⊆ subset relation
S1 and S2 must have the same type
S1 ⊆ S2 ⇔ (∀ x : S1 | x ∈ S2 )

P power set operator

S0 ∈ P S ⇔ S0 ⊆ S

× cartesian product
(x1 , . . . , xn ) ∈ S1 × . . . × Sn ⇔ (x1 ∈ S1 ∧ . . . ∧ xn ∈ Sn )

B. Beckert: Formal Specification of Software – p.9

Set Operations

∪, ∪ union
Involved sets must have the same type T
x ∈ S1 ∪ S2 ⇔ (x ∈ S1 ∨ x ∈ S2 )

x ∈ ∪ S ⇔ (∃ S0 : T • x ∈ S0 )

∩, ∩ intersection

\ set difference

B. Beckert: Formal Specification of Software – p.10

Types

Pre-defined types

Z with constants: 0, 1, 2, 3, 4, . . .
functions: +, −, ∗, /
predicates: <, ≤, >, ≥

Sets
Every set can be used as a type

Basic types (given sets)

Example

[Person]

B. Beckert: Formal Specification of Software – p.11

Free Type Definitions

Example
weekDay ::= mon | tue | wed | thu | fri | sat | sun

Example
Tree ::= leaf hhZii | nodehhTree × Treeii

Meaning

[Tree] generated by leaf , node

∀ x1 , y1 , x2 , y2 : Tree | node(x1 , y1 ) = node(x2 , y2 ) • (x1 = x2 ∧ y1 = y2 )

∀ x1 , x2 : Z | leaf (x1 ) = leaf (x2 ) • x1 = x2
∀ x : Z; y, z : Tree • leaf (x) 6= node(y, z)

Note: Generatedness is not expressible in first-order logic

B. Beckert: Formal Specification of Software – p.12
Compound Types

Set type: PT
The type of sets of elements of type T

Cartesian product type: T 1 × · · · × Tn

The type of tuples (t1 , . . . , tn ) with ti ∈ Ti

B. Beckert: Formal Specification of Software – p.13

Types: Overview

Possible type definitions

T=Z

T = [Type]

T ::= . . . (free type)

T = P T0

T = T1 × · · · × T n

B. Beckert: Formal Specification of Software – p.14

Types: Overview

Possible type definitions

T=Z

T = [Type]

T ::= . . . (free type)

T = P T0

T = T1 × · · · × T n

Note
All types are disjoint (not for sets that are used as types)
All terms have a unique type
B. Beckert: Formal Specification of Software – p.14
Variables

Variable declarations
Example

x:Z
sold : P Seat

Variables can range over types and over sets

B. Beckert: Formal Specification of Software – p.15

Syntactical Abbreviations

Abbreviations

must not be recursive

can be generic

Examples
numberPairs == Z × Z

pairWithNumber[S] == Z × S

Note
Type variables are “meta-variables” (cannot be quantified)

B. Beckert: Formal Specification of Software – p.16

Abbreviations vs. Generated Types

weekDay1 == {mon, tue, wed, thu, fri, sat, sun}

vs.

WeekDay2 ::= mon | tue | wed | thu | fri | sat | sun

B. Beckert: Formal Specification of Software – p.17

Abbreviations vs. Generated Types

weekDay1 == {mon, tue, wed, thu, fri, sat, sun}

vs.

WeekDay2 ::= mon | tue | wed | thu | fri | sat | sun

Not the same

Type definition implies elements to be different

B. Beckert: Formal Specification of Software – p.17

Axiomatic Definitions

Form of an axiomatic definition

SymbolDeclarations
ConstrainingPredicates

Example
N1 : P Z
∀ z : Z • (z ∈ N1 ↔ z ≥ 1)

B. Beckert: Formal Specification of Software – p.18

Relations

Relation types/sets
S ↔ T is the type/set of relations between types/sets S and T
S ↔ T = P(S × T)

Notation
a 7→ b for (a, b) if (a, b) ∈ S ↔ T

B. Beckert: Formal Specification of Software – p.19

Operations on Relations

Domain dom R

dom R = {a : S, b : T | a 7→ b ∈ R • a}

Range ran R

ran R = {a : S; b : T | a 7→ b ∈ R • b}

B. Beckert: Formal Specification of Software – p.20

Operations on Relations

Domain dom R

dom R = {a : S, b : T | a 7→ b ∈ R • a}

Range ran R

ran R = {a : S; b : T | a 7→ b ∈ R • b}

Restrictions of relations

S0 C R = {a : S; b : T | a 7→ b ∈ R ∧ a ∈ S0 • a 7→ b}

R B T 0 = {a : S; b : T | a 7→ b ∈ R ∧ b ∈ T 0 • a 7→ b}

S0 −
C R = {a : S; b : T | a 7→ b ∈ R ∧ a 6∈ S0 • a 7→ b}

B T 0 = {a : S; b : T | a 7→ b ∈ R ∧ b 6∈ T 0 • a 7→ b}
R−

B. Beckert: Formal Specification of Software – p.20

Operations on Relations

Inverse relation R−1

R−1 = {a : S; b : T | a 7→ b ∈ R • b 7→ a}

B. Beckert: Formal Specification of Software – p.21

Operations on Relations

Inverse relation R−1

R−1 = {a : S; b : T | a 7→ b ∈ R • b 7→ a}

Composition R o9 R0 R : S ↔ T and R0 : T ↔ U
R o9 R0 = {a : S; b : T; c : U | a 7→ b ∈ R ∧ b 7→ c ∈ R0 • a 7→ c}

B. Beckert: Formal Specification of Software – p.21

Operations on Relations

Inverse relation R−1

R−1 = {a : S; b : T | a 7→ b ∈ R • b 7→ a}

Composition R o9 R0 R : S ↔ T and R0 : T ↔ U
R o9 R0 = {a : S; b : T; c : U | a 7→ b ∈ R ∧ b 7→ c ∈ R0 • a 7→ c}

Closures R:S↔S
iteration Rn = R o9 Rn−1
identity R0 = {a : S | true • a 7→ a}
refl./trans. R∗ = ∪{n : N | true • Rn }
transitive R+ = ∪{n : N | n ≥ 1 • Rn }
symetric R s = R ∪ R −1
reflexive R r = R ∪ R0

B. Beckert: Formal Specification of Software – p.21

Functions

Special relations
Functions are special relations

Notation
Instead of ↔

→ total function
→
7 partial function

B. Beckert: Formal Specification of Software – p.22

Functions

Partial functions

f ∈S→ 7 T ⇔
f ∈S↔T ∧
∀ a : S, b : T , b0 : T | (a 7→ b ∈ f ∧ a 7→ b0 ∈ f ) • b = b0

B. Beckert: Formal Specification of Software – p.23

Functions

Partial functions

f ∈S→ 7 T ⇔
f ∈S↔T ∧
∀ a : S, b : T , b0 : T | (a 7→ b ∈ f ∧ a 7→ b0 ∈ f ) • b = b0

Total functions

f ∈S→T ⇔
f ∈S→ 7 T ∧
∀ a : S • ∃ b : T • a 7→ b ∈ f

B. Beckert: Formal Specification of Software – p.23

λ Notation for Functions

General form

λa : S | p • e

Example
double : Z →
7 Z
double = λ n : Z | n ≥ 0 • n + n

Equivalent to

double : Z →
7 Z
double = {n : N | true • n 7→ n + n}

B. Beckert: Formal Specification of Software – p.24

Prefix and Infix Notation

Notation
Relations and functions can be declared prefix and infix
Parameter positions are indicated with “ ”

Example
even : P Z
∀ x : Z • (even x ⇔ (∃ y : Z • x = y + y))

Equivalent to

even : P Z
even = {x : Z | (∃ y : Z • x = y + y)}

B. Beckert: Formal Specification of Software – p.25

More Notation for Functions

Notation

7
partial injective function
total injective function
→
→
7 partial surjective function
→
→ total surjective function
→
total bijective function

B. Beckert: Formal Specification of Software – p.26

Three Definitions of abs

Relation (in infix notation)

abs : Z ↔ N
∀ m : Z, n : N • (m abs n) ↔ (m = n ∨ −m = n)

B. Beckert: Formal Specification of Software – p.27

Three Definitions of abs

Relation (in infix notation)

abs : Z ↔ N
∀ m : Z, n : N • (m abs n) ↔ (m = n ∨ −m = n)

Function

abs : Z → Z
abs = (λ m : Z | m ≤ 0 • −m) ∪ (λ m : Z | m ≥ 0 • m)

B. Beckert: Formal Specification of Software – p.27

Three Definitions of abs

Relation (in infix notation)

abs : Z ↔ N
∀ m : Z, n : N • (m abs n) ↔ (m = n ∨ −m = n)

Function

abs : Z → Z
abs = (λ m : Z | m ≤ 0 • −m) ∪ (λ m : Z | m ≥ 0 • m)

Function (in prefix notation)

abs : Z →
7 Z
∀ x : Z | x ≤ 0 • x = −(abs x)
∀ x : Z | x ≥ 0 • x = abs x

B. Beckert: Formal Specification of Software – p.27

Finite Constructs

Finite subsets of Z

m..n = {n0 : N | m ≤ n0 ∧ n0 ≤ n}

B. Beckert: Formal Specification of Software – p.28

Finite Constructs

Finite subsets of Z

m..n = {n0 : N | m ≤ n0 ∧ n0 ≤ n}

Finite sets
F T consists of the finite sets in P T
[S]
F : P(P S)
F = {s : P S | (∃ n : N • (∃ f : 1..n
→ s • true))}

B. Beckert: Formal Specification of Software – p.28

Finite Sets: Cardinality

Cardinality operator #
[S]
# : FS → N
∀ s : F S; n : N • (n = #s ↔ (∃ f : 1..n
→ s • true))

B. Beckert: Formal Specification of Software – p.29

Finite Functions

Notation

→
77 finite (partial) functions (e.g. arrays)

7 7 T = {f : S →
S→ 7 T | dom f ∈ F S}

77
finite (partial) injective functions (e.g. duplicate-free arrays)

7 7 T = {f : S
S 7 T | dom f ∈ F S}

B. Beckert: Formal Specification of Software – p.30

Sequences

Definition

seq T == {s : Z →
7 7 T | dom s = 1..#s}

Note

sequences are functions, which are relations, which are sets

the length of s is #s

B. Beckert: Formal Specification of Software – p.31

Sequences

Definition

seq T == {s : Z →
7 7 T | dom s = 1..#s}

Note

sequences are functions, which are relations, which are sets

the length of s is #s

Notation
The sequence {1 7→ x1 , 2 7→ x2 , . . . , n 7→ xn }
is written as hx 1 , x 2 , . . . , x n i

B. Beckert: Formal Specification of Software – p.31

Example: Concatenation of Sequences

s a t ==
s ∪
(λ n : Z | n ∈ #s + 1..#s + #t • n − #s) o
9 t

B. Beckert: Formal Specification of Software – p.32

Schemata

General form

Name
SymbolDeclarations
ConstrainingPredicates

Linear notation

b [SymbolDeclarations | ConstrainingPredicates]
Name =

B. Beckert: Formal Specification of Software – p.33

Schemata

With empty predicate part

Name
SymbolDeclarations

Linear notation

b [SymbolDeclarations]
Name =

B. Beckert: Formal Specification of Software – p.34

Schemata: Example

Theater tickets

[Seat]
[Person]

TicketsForPerformance0
seating : P Seat
sold : Seat →7 Person
dom sold ⊆ seating

B. Beckert: Formal Specification of Software – p.35

Schemata as Sets/Types

Schema

Name
x1 : T 1
...
xn : T n
ConstrainingPredicates

can be seen as the following set (type) of tuples:

Name =
{x1 : T1 ; . . . ; xn : Tn | ConstrainingPredicates • (x1 , . . . , xn )}

B. Beckert: Formal Specification of Software – p.36

Schema Inclusion

Inclusion
Schemata can be used (included) in
– schema
– set comprehension
– quantification
by adding the schema name to the declaration part

Meaning
– declarations
– constraining predicates
are added to the corresponding parts of the including
schema / set comprehension / quantification
Note: Matching names merge and must be type compatible

B. Beckert: Formal Specification of Software – p.37

Schema Inclusion

Example
NumberInSet
a:Z
c : PZ
a∈c

{NumberInSet | a = 0 • c}

is the same as

{a : Z, c : P Z | a ∈ c ∧ a = 0 • c}

(the set of all integer sets containing 0)

B. Beckert: Formal Specification of Software – p.38

Schemata as Predicates

Schemata can be used as predicates in

– schema
– set comprehension
– quantification
by adding the schema name to the predicate part
(occurring variables must already be declared)

Meaning
The constraining predicates (not: the declaration part)
are added to the corresponding part of the
schema / set comprehension / quantification

B. Beckert: Formal Specification of Software – p.39

Schemata as Predicates

Example
NumberIn01
a:Z
c : PZ
a∈c
c ⊆ {0, 1}

∀ a : Z; c : P Z | NumberIn01 • NumberInSet

is the same as

∀ a : Z; c : P Z | a ∈ c ∧ c ⊆ {0, 1} • a ∈ c

B. Beckert: Formal Specification of Software – p.40

Generic Schemata

Type/set variables can be used in schema definitions

Example
NumberInSetGeneric[X]
a:X
c : PX
a∈c

Then

NumberInSetGeneric[Z] = NumberInSet

B. Beckert: Formal Specification of Software – p.41

Variable Renaming in Schemata

Variables in schemata can be renamed

Example
NumberInSet[a/q, c/s]

is equal to

q:Z
s : PZ
q∈s

B. Beckert: Formal Specification of Software – p.42

Conjunctions of Schemata

Schemata can be composed conjunctively

Example
Given
ConDis1 ConDis2
a : A; b : B b : B; c : C
P Q

Then the following are equivalent

ConDis1 ∧ ConDis2
a : A; b : B; c : C
P
Q

B. Beckert: Formal Specification of Software – p.43

Disjunctions of Schemata

Schemata can be composed disjunctively

Example
Given
ConDis1 ConDis2
a : A; b : B b : B; c : C
P Q

Then the following are equivalent

ConDis1 ∨ ConDis2
a : A; b : B; c : C
P∨Q

B. Beckert: Formal Specification of Software – p.44

Example

Informal specification
Theater: Tickets for first night are only sold to friends

Specification in Z
Status ::= standard | firstNight

Friends
friends : P Person
status : Status
sold : Seat →7 Person
status = firstNight ⇒ ran sold ⊆ friends

B. Beckert: Formal Specification of Software – p.45

Example

TicketsForPerformance1 =
b TicketsForPerformance0 ∧ Friends

and

TicketsForPerformance1
Friends
TicketsForPerformance0

B. Beckert: Formal Specification of Software – p.46

Example

TicketsForPerformance1 =
b TicketsForPerformance0 ∧ Friends

and

TicketsForPerformance1
Friends
TicketsForPerformance0

are the same as

TicketsForPerformance1
friends : P Person; status : Status
sold : Seat →7 Person; seating : P Seat
status = firstNight ⇒ ran sold ⊆ friends
dom sold ⊆ seating

B. Beckert: Formal Specification of Software – p.46

Normalisation of Schemata

Normalisation
A schema is normalised if in the declaration part

Variables are typed

but not restricted to subsets of types

B. Beckert: Formal Specification of Software – p.47

Normalisation of Schemata

Normalisation
A schema is normalised if in the declaration part

Variables are typed

but not restricted to subsets of types

Example
The normalisation of is

x:N x:Z
P x≥0
P

B. Beckert: Formal Specification of Software – p.47

Negation of Schemata

A schema is negated by negating the predicate part in

its normalised form

Example
The negation of is the negation of

x:N x:Z
P x∈N
P
which is

x:Z
¬ (x ∈ N ∧ P)

B. Beckert: Formal Specification of Software – p.48

Schemata as Operations

States
A state is a variable assignment
A schema describes a set of states

Operations
To describe an operation,
a schema must describe pairs of states (pre/post)

B. Beckert: Formal Specification of Software – p.49

Schemata as Operations

States
A state is a variable assignment
A schema describes a set of states

Operations
To describe an operation,
a schema must describe pairs of states (pre/post)

Notation
Variables are decorated with 0 to refer to their value in the post state
Whole schemata can be decorated

B. Beckert: Formal Specification of Software – p.49

Schemata as Operations

Example
NumberInSet0

is the same as

NumberInSet0
a0 : Z
c0 : P Z
a0 ∈ c0

B. Beckert: Formal Specification of Software – p.50

Schemata as Operations

Example
NumberInSet0

is the same as

NumberInSet0
a0 : Z
c0 : P Z
a0 ∈ c0

Further decorations

input variables are decorated with “?”

output variables are decorated with “!”
B. Beckert: Formal Specification of Software – p.50
Example

Theater: Selling tickets

Purchase0
TicketsForPerformance0
TicketsForPerformance00
s? : Seat
p? : Person
s? ∈ seating\ dom sold
sold0 = sold ∪ {s? 7→ p?}
seating0 = seating

(no output variables in this schema)

B. Beckert: Formal Specification of Software – p.51

Example

Response ::= okay | sorry

Success
r! : Response
r! = okay

Then

Purchase0 ∧ Success

is a schema that reports successful ticket sale

B. Beckert: Formal Specification of Software – p.52

Schemata as Operations: General Form

StateSpace
x1 : T 1 ; . . . ; x n : T n
inv(x1 , . . . , xn )

Operation
StateSpace
StateSpcae0
i1 ? : U 1 ; . . . ; i m ? : U m
o1 ! : V 1 ; . . . ; o p ! : V p
pre(i1 ?, . . . , im ?, x1 , . . . , xn )
op(i1 ?, . . . , im ?, x1 , . . . , xn , x10 , . . . , xn0 , o1 !, . . . , op !)

B. Beckert: Formal Specification of Software – p.53

The ∆ Operator

Definition
∆Schema abbreviates Schema ∧ Schema 0

General form of operation schema using ∆

Operation
∆StateSpace
i1 ? : U 1 ; . . . ; i m ? : U m
o1 ! : V 1 ; . . . ; o p ! : V p
pre(i1 ?, . . . , im ?, x1 , . . . , xn )
op(i1 ?, . . . , im ?, x1 , . . . , xn , x10 , . . . , xn0 , o1 !, . . . , op !)

B. Beckert: Formal Specification of Software – p.54

The Ξ Operator

Definition
ΞSchema abbreviates ∆Schema ∧ (x1 = x10 ∧ . . . ∧ xn = xn0 )
where x1 , . . . xn are the variables declared in Schema

General form of operation schema using Ξ

Operation
ΞStateSpace
i1 ? : U 1 ; . . . ; i m ? : U m
o1 ! : V 1 ; . . . ; o p ! : V p
pre(i1 ?, . . . , im ?, x1 , . . . , xn )
op(i1 ?, . . . , im ?, x1 , . . . , xn , o1 !, . . . , op !)

Using Ξ indicates that the operation does not change the state
B. Beckert: Formal Specification of Software – p.55
The Operators ∆ and Ξ: Example

The following schemata are equivalent

ΞNumberInSet

∆NumberInSet
a = a0
c = c0

NumberInSet
NumberInSet0
a = a0
c = c0
B. Beckert: Formal Specification of Software – p.56
Example

Theater: Selling tickets, but only to friends if first night performance

Purchase1
∆TicketsForPerformance1
s? : Seat
p? : Person
s? ∈ seating\ dom sold
status = firstNight ⇒ (p? ∈ friends)
sold0 = sold ∪ {s? 7→ p?}
seating0 = seating
status0 = status
friends0 = friends

B. Beckert: Formal Specification of Software – p.57

Example

NotAvailable
ΞTicketsForPerformance1
s? : Seat
p? : Person
s? ∈ dom sold ∨ (status = firstNight ∧ ¬ p? ∈ friends)

Failure
r! : Response
r! = sorry

TicketServiceForPerformance =b
(Purchase1 ∧ Success) ∨
(NotAvailable ∧ Failure)

B. Beckert: Formal Specification of Software – p.58

Quantifying (Hiding) Variables in Schemata

Schema quantification
∀ x : S • Schema resp.
∃ x : S • Schema

(existential quantification is also called “variable hiding”)

B. Beckert: Formal Specification of Software – p.59

Quantifying (Hiding) Variables in Schemata

Schema quantification
∀ x : S • Schema resp.
∃ x : S • Schema

(existential quantification is also called “variable hiding”)

Example
∃ a : Z • NumberInSet

is the same as

c : PZ
∃a : Z • a ∈ c

B. Beckert: Formal Specification of Software – p.59

Composition of Operation Schemata

Definition
Operation schemata can be composed using o9, where

every variable with 0 in the first schema must occur without 0

in the second schema
these variables are identified and
hidden from the outside

B. Beckert: Formal Specification of Software – p.60

Composition: General form

Op1 Op2
x1 : T 1 ; . . . ; x p : T p y1 : U 1 ; . . . ; y q : U q
z1 : V 1 ; . . . ; z n : V n z1 : V 1 ; . . . ; z n : V n
z10 : V1 ; . . . ; zn0 : Vn z10 : V1 ; . . . ; zn0 : Vn
op1(x1 , . . . , xp , op2(y1 , . . . , yq ,
z1 , . . . , zn , z10 , . . . , zn0 ) z1 , . . . , zn , z10 , . . . , zn0 )

Op1 o9 Op2
x1 : T 1 ; . . . ; x p : T p
y1 : U 1 ; . . . ; y q : U q
z1 : V 1 ; . . . ; z n : V n
z10 : V1 ; . . . ; zn0 : Vn
∃ z100 : V1 ; . . . ; zn00 : Vn •
op1(x1 , . . . , xp , z1 , . . . , zn , z100 , . . . , zn00 )
op2(y1 , . . . , yq , z100 , . . . , zn , z10 , . . . , zn0 )
B. Beckert: Formal Specification of Software – p.61
Example

Purchase1 o
9 Purchase1[s?/s2?]

is equivalent to

∆TicketsForPerformance1
s? : Seat; s2? : Seat; p? : Person
s? ∈ seating\ dom sold
s2? ∈ seating\ dom(sold ∪ {s? 7→ p?})
status = firstNight ⇒ (p? ∈ friends)
sold0 = sold ∪ {s? 7→ p?, s2? 7→ p?}
seating0 = seating
status0 = status
friends0 = friends

B. Beckert: Formal Specification of Software – p.62