Transcript Z Notation

CEIT
AUT
Requirements Specification and
Verification Using Z
A. Rasoolzadegan
July, 2009
1
Z (pronounced `zed') - Introduction

Named after Zermelo-Fränkel set theory

A formal specification language based on set theory and first order
predicate logic

Makes it easier to write mathematical description of complex
dynamic systems such as software ,

Originally proposed by Abrial in 1977 with the help of Steve
Schuman and Bertrand Meyer

Developed further at the Programming Research Group at the
Oxford University Computing Laboratory (OUCL) and elsewhere
since the late 1970s,
2
Introduction (Cont.)

Mathematical Language

set theory


mathematical logic


standard set operators, set comprehensions, Cartesian products, and
power sets.
first order predicate calculus
Schemas language

used to describe

the state of a system,

the ways in which that state may change

system properties
3
Introduction (Cont.)

We may refine a specification, yielding another description that is
closer to executable code,

We may reason about these specifications using the proof techniques
of mathematical logic,

Z is not intended for the description of non- functional properties
neither for timed & concurrent behavior

Various tools for formatting, type-checking and aiding proofs in Z are
available,

The ISO completed a Z standardization effort in 2002
4
The importance of proof

At the specification stage:



At the design stage:



can show us not only that a design is correct,
but also why it is correct.
At the implementation stage:


help us to understand the requirements upon a system, and
can assist us in identifying any hidden assumptions
help us to ensure that a piece of code behaves according to the
specification
A significant contribution to quality improvement
5
The importance of proof (Cont.)

A specification without proofs

is untested:

it may be inconsistent;

it may describe properties that were not intended, or omit
those that were;

it may make inappropriate assumptions.
6
The logical language of Z

Propositional Logic

Predicate Logic
7
Propositional Logic
Propositional connectives
8
Propositional Logic (Cont.)

These inference rules form part of the natural deduction
system that we use to conduct our proofs:
modus ponens rule
9
Propositional Logic (Cont.)
10
Exp. Disjunction is commutative:
Proof:
11
Proof:
12
Proof:
13
Proof:
14
The logical language of Z
 Propositional Logic

Predicate Logic
15
Predicate Logic

Is a powerful technique to expressing the universal and
existential statements (quantified predicates)
16
Predicate Logic (Cont.)
A special case:
17
Predicate Logic (Cont.)
A special case:
18
to denote the unique object x from a such that p
19
Set Theory

Mathematical objects are often seen as well-defined collections of other
objects

The Z notation is based upon set theory

Specifications in Z find their meanings as operations upon sets

All the set theory we require for specification, refinement, and proof:
 the notions of





set membership,
extension,
Comprehension,
the power set and
Cartesian product constructors.
the set of finite subsets of a
20
Set Theory (Cont.)


Some axioms of Zermelo-Fraenkel set theory:
This inference rule is supported by two axioms of
Zermelo-Fraenkel (specification & replacement):
21
Set Theory (Cont.)
22
Exp.
Proof:
23
Object Definition in Z

In the Z notation, there are several ways of defining an
object:

declarations,

abbreviations,

axioms,

free types and

schemas.
24
Object Definition in Z - Declarations

The simplest way to define an object

If the object is a given set, or basic type:


introduces a new basic type called Type
If the object is a variable:

introduces a new variable x, drawn from the set A

If this set is not Z, it must be defined elsewhere in the
specification
25
Object Definition in Z - Abbreviations

Introduces a new name for term:

Generic abbreviations:
26
Object Definition in Z - Axiomatic definitions

where the predicate expresses the constraints upon the
object or objects introduced in the declaration.

Axiomatic definition of the set of natural numbers:
27
Object Definition in Z - Axiomatic definitions
Generic definitions:
Exp. Generic definition to define the subset symbol:
28
Proof:
29
Relations

In a formal specification, it is often necessary to describe
relationships between objects

Binary Relations:

Elements of relations:

If R is a relation of type
X , then
, and A is any subset of
denotes the domain restriction of R to A:
30
Relations (Cont.)

If B is any subset of Y , then
denotes the range
restriction of R to B:

domain subtraction of A from R

range subtraction of B from R:
31
Relations (Cont.)

If R is a relation of type
X , then
, and A is any subset of
denotes the relational image of A under R:

Relational inverse:

Relational composition:
32
Functions

Partial functions:

Total functions:
33
Functions (Cont.)
34
Functions (Cont.)

Function description using Lambda notation:
35
Functions on relations
36
Functions (Cont.)


Overriding:
Set of all finite functions from A to B:
37
Properties of functions
38
Functions (Cont.)

Size/Cardinality:
39
Sequences

If X is a set, then the set of all finite sequences of objects from X is
defined by the following abbreviation:
40
Sequences (Cont.)
Filter:
41
Functions on sequences
Using recursion principle:
Exp.
42
Proof:
43
Structural induction
Construct a proof that filter is distributive using structural induction:
Inductive hypothesis:
Induction:
44
Proof Lemma1 & Lemma2 using the following rules:
Lemma1
Lemma2
45
Object Definition in Z

In the Z notation, there are several ways of defining an
object:

declarations,

abbreviations,

axioms,

free types and

schemas.
46
Free Types
Exp. 1:
Exp. 2:
recursive type definition
Exp. 3:
47
Free Types (Cont.)
axiomatic definition:
constants
constructor functions
• Any subset of T that contains all of the constants and is closed
under the constructors must be the whole of T.
• A set S is closed under d and E if the image of E.S = T. under d is
48
within S itself.
Object Definition in Z

In the Z notation, there are several ways of defining an
object:

declarations,

abbreviations,

axioms,

free types and

schemas.
49
Schemas
Exp:
51
Schemas (Cont.)


In our mathematical language, there are four ways of
introducing a type:

as a given set,

as a free type,

as a power set, or

as a Cartesian product.
If we require a composite type, one with a variety of
different components, then the schema language offers a
useful alternative:
S: SchemaOne
S.a S.c
52
Schemas (Cont.)
Schemas as declarations
53
Schemas (Cont.)
Characteristic binding:
54
Schemas (Cont.)
Call: free
Generic schemas:
If we choose Z to be the actual parameter, we
obtain a schema that is equivalent to SchemaTwo
55
Schema Operators
Conjunction & Disjunction
• allows us to specify different aspects of a specification
separately, and then combine them to form a complete description
56
Schema Operators (Cont.)
Exp:
57
Schema Operators (Cont.)
58
Decoration


To describe an operation upon the state, we use two copies of State:

One representing the state before the operation;

the other representing the state afterwards.
Decorate the components of the second schema, adding a single prime
to each name:
59
Decoration (Cont.)
60
Schema Operators (Cont.)
Quantification:
universal quantification
existential quantification
hiding
61
Promotion / framing
62
Predicate part of
AnswerGlobal
Predicate part of
63
Promotion / framing (Cont.)
64
Free promotion
A promotion is said to be free if and only if the promotion schema satisfies
An example of a free promotion:
65
A promotion that is not free is said to be constrained.
An example of a constrained promotion:
66
Proof opportunities arising from A.D.T.

The construction of an abstract data type presents two important proof opportunities:

a demonstration that the various requirements upon the data type are consistent and not
contradictory.

a demonstration that each operation is never applied outside its domain, in a situation for which
the results of the operation are not defined.

In the Z notation, we use the language of schemas to construct the data type

To show ,we have only to show that the constraint part of the state schema is
satisfiable.

This is usually achieved by proving an initialisation theorem:


we show that an initial state, at least, exists.
To show ,we must investigate their preconditions.
67
The initialisation theorem

The state of the system is modeled as an object of schema
type, the predicate part of which represented a state
invariant:


If the predicate part includes a contradiction, then the data
type description is vacuous:


a list of requirements that should be true in any valid state
it is impossible to fulfil the requirements, therefore no state exists.
To fulfil the requirements, it is enough to establish that at
least one state exists.
68
1. The initialisation theorem (Cont.)
69
1. The initialisation theorem (Cont.)
The initialisation theorem is therefore
Now the initialisation theorem should be proved
70
1. The initialisation theorem (Cont.)
Proof:
71
2. Precondition investigation
72
73
2. Precondition investigation (Cont.)
74
2. Precondition investigation (Cont.)
Exp:
75
2. Precondition investigation (Cont.)
76
2. Precondition investigation (Cont.)
77
2. Precondition investigation (Cont.)
78
2. Precondition investigation (Cont.)
79
2. Precondition investigation (Cont.)
If Promote is free then:
80
Case Study: A File System

We show how the schema notation can be used to
specify a simple file system:

Representing concrete data structures and a set of
operations upon them,

We show also how the preconditions of the various
operations can be calculated,

How the description of a single file can be promoted to
an indexed component of a file system
81
A programming interface

To set down exactly what it is that we intend to
model:


a list of operations upon the file system,

complete with a description of their intended affects.
We may divide the operations into two groups:

those that affect the data within a single file,

those that affect the file system as a whole.
82
A programming interface (Cont.)

At the file level, there are four operations:

read: used to read a piece of data from a file;

write: used to write a piece of data to a file;


add: used to add a new piece of data to a file;


overwrite an existing part of the file
extend the file to accommodate the new data
delete: used to delete a piece of data from a file.
83
A programming interface (Cont.)

At the file system level, there are four operations:

create: used to create a new file;

destroy: used to destroy an existing file;

open: used to make a file available for reading and
writing of data;

close: used to make a file unavailable for reading and
writing.
84
Operations upon files
storage keys
data elements
85
Operations upon files (Cont.)
86
Operations upon files (Cont.)
87
A more complete description

A failed operation upon the file state will always
produce a report as output:
88
A more complete description (Cont.)
89
A more complete description (Cont.)

A successful operation will always produce a
report of the same value:
90
A more complete description (Cont.)
91
A file system

A file system contains a number of files indexed
using a set of names.
92
A file system (Cont.)

We may choose to promote the operations defined
above.

The local state is described by File,

The global state is described by System,

and the promotion is characterized by the schema
Promote:
93
A file system (Cont.)
94
A file system (Cont.)

We define four operations using this promotion:
95
96
97
A file system (Cont.)

We will now extend our free type of report
messages to take account of the errors that may
occur in file access and file management
operations:
98
99
A file system (Cont.)
100
The final formal description of the file system.
101
Formal Analysis
1. Initialisation theorem:

To check that our state invariant contains no contradictions
there exists a binding of file and open which satisfies the
constraint part of SystemInit
102
Initialisation theorem
Proof:
103
Initialisation theorem (Cont.)

Since we are using File as a type, we should also prove
that:
Proof:
104
Formal Analysis (Cont.)
2. Precondition investigation:
As an example, consider the operation KeyRead,
defined by:
105
Precondition investigation (Cont.)
1:
106
Precondition investigation (Cont.)
2:
107
Precondition investigation (Cont.)
3:
This is a free promotion
108
Precondition investigation (Cont.)
109
Precondition investigation (Cont.)
110
Precondition investigation (Cont.)

For each operation, we list the partial operations used in
its definition, together with their preconditions. In every
case, the disjunction of these preconditions is true

our operations are total.
111
Data Refinement

Refinement:

Developing a specification in such a way that it leads us towards a
suitable implementation


by adding more information in each step of refinement.
The process of improvement involves the removal of indeterminism,
or uncertainty.

The refinement must be correct

It is important that our new, more detailed description is consistent
with our original specification:
112
Relations and indeterminism

Total relations:

If R and S are total relations, then R refines S exactly
when

Wherever S relates the same element x to two distinct
elements y1 and y2 , R may remove a degree of
uncertainty by omitting either
113
Relations and indeterminism (Cont.)

Partial relations:

we may consider their totalised versions

If is a partial relation between types X and Y then:
114
Relations and indeterminism (Cont.)
115
Relations and indeterminism (Cont.)

If
are two partial relations of the same
type, then
refines
precisely when
116
Relations and indeterminism (Cont.)
The changesto is a refinement of the corruptsto
117
Data types and data refinement


A data type X is a tuple
, where:
Both xi and xf are total, but each xoi may be partial
118
Data types and data refinement (Cont.)

A program is a sequence of operations upon a data type.

It may be seen as a relation between input and output,
recorded by the initialisation and finalisation steps at the
beginning and end of this sequence

Exp.
is a program that uses the data type
119
Data types and data refinement (Cont.)

The choice of data representation within the data
type is not relevant to the overall behaviour of the
program

It is encapsulated by initialisation and finalisation.

Thus programs may be parameterised by data
types:
120
Data types and data refinement (Cont.)
An abstract data type X may be totalised:
If data types A and C share the same indexing set, then A is
refined by C if and only if for each program P(A):
If A and C are both indexed by the set I , then this definition
requires us to prove that, for sequences
in seq I
In practice, this may be a difficult result to establish
121
Simulations
122
Simulations (Cont.)

If data types A and C share the same indexing set,
then the programs P(A) and P(C) will have the
same number of steps:

One for each operation involved.

We may therefore compare the two programs on a step-
by-step basis.
123
Simulations (Cont.)
124
Forwards/Downwards Simulation
125
Forwards Simulation (Cont.)
126
Backwards/Upwards Simulation
127
Backwards/Upwards Simulation
128
Relaxing and unwinding

By considering domain and range restrictions, we can
obtain an equivalent set of requirements that mention
neither totalisation nor lifting.

These requirements constitute a more relaxed set of rules
for data refinement.
129
Relaxed rules for simulations
130
Specification statements

To describe operations upon an abstract data type
we may use

Schemas

Specification statements:

abstract programs consisting of

a precondition,

a postcondition,

a list of variables.
131
Specification statements (Cont.)

Describes an operation that

begins in a state satisfying precondition,

ends in a state satisfying postcondition,

only those variables listed in frame are affected.
132
Specification statements (Cont.)
133
Specification statements (Cont.)

The following specification statement describes the
operation of finding an approximate root for a function.

a value m such that f (m) is close to zero.

within a particular interval [a,b].

It will fail if no such value exists:
134
Assignment

A program in the refinement calculus may consist
of a mixture of specification statements and code.
135
Refinement of Specification statements

If a program P is correctly refined by another
program Q, then we write:
136
Refinement of Specification statements (Cont.)
Exp.
137
Refinement of Specification statements (Cont.)
Exp.
138
Refinement of Specification statements (Cont.)

Suppose that we want to swap two variables without
using a third variable to store the intermediate value:
139
140
Conditional statements
141
Iteration
142
References

Jim Davies and Jim Woodcock, Using Z: Specification, Refinement and
Proof, Prentice Hall International Series in Computer Science, 1996, ISBN
0-13-948472-8.

Gerard O’Regan, Mathematical Approaches to Software Quality, Springer
–Verlag London Limited, 2006, ISBN -13: 978-1-84628-242-3.
143
Thank you for your attention!
Questions ???
?
144