INTRDUCTION TO

Z SPECIFICATIONS
Formal Methods
BCS 2213
Semester 1 Session 2016/2017
 What is Z
2

 First off – its pronounced Zed

 After the Zermelo-Fränkel set theory
 Z is mathematical notation based on set
theory, first order predicate logic and lambda
calculus.
 It has been initially developed at
the Computing Laboratory of Oxford University
and next elsewhere since the middle of 1980.
 What is Z
3

 Z – is a modelling notation used to model the

behavior of a system.
 Z models a system by representing its state (a
collection of state variables and their values)
and operations that may change the state.
 Can be used to represent structure of software
code: data types, procedures, functions,
modules, classes, objects etc.
 Z is not software or executable code.
 Z is….
4

 Z describes “what” the system must do without

saying “how” it is to be done.
 Z is just a notation, it is not a method.
 Z can support many different methods.
 Z is suitable for
 Procedural programming
 Object-oriented programming. There are object
oriented languages that extend Z (Object-Z, Z++ )
 Functional programming
 Z is…
5

 Designed for people not machines

 Z notation is a mixture of boxes, text, Greek
letters and invented pictorial symbols.
 Includes two notations
 Notation to express ordinary discrete mathematics
 Notation to structure mathematical text (by schemas).

 Problems with Z notation

 Z notation uses many non-ASCII symbols
 The specification includes rules for rendering the Z
notation symbols in ASCII as well as LaTeX.
CZT-IDE for Z

 You may download it from

http://sourceforge.net/projects/czt/files/czt-ide/2.0-pre1/
 Z mathematical tool-kit
7

 Collection of mathematical objects and

operators : definitions and laws concerning
sets, tuples, relations, functions, sequences
and their operators.
 Plays the same role as standard library of
types and functions in programming.
 Sample of Z Mathematical tool-kit :
http://staff.washington.edu/jon/z/toolkit.html
 Elements of Z: Sets
8

A set is a collection of distinct objects (elements)

Order of these objects is not significant
A set can have two or more identical elements

{ 1, 2, 3, 4, 5, 6 }  The Null Set or

{ 4, 5, 6, 1, 2, 3 } Empty Set. This
{ 4, 4, 5, 5, 6, 6, 1, 2, 3 } is a set with no
elements
{ i: |1≤i≤6 }
{ red, yellow, green }
Notation. Usually we denote sets with upper-case
letters, elements with lower-case letters.
 Elements of Z - Types
9

Every object in Z belongs to a set called its type.

E.g. {…-1, 0, 1, 2,...} belong to the basic type .
- is the set of integers.

{ red, yellow, green } belong to the free (user

defined) type COLOR. Free types in Z are like
enumerations in programming languages.
COLOR ::= red | green | yellow

Every free type must be introduced in a declaration.

 Elements of Z – Basic types
10

ℝ - The set of real numbers

 Elements of Z – Compound Types
11

Compound set type: T

The type of the set of sets of the elements of the type T
 Elements of Z - Variables
12

A variable is a name for an object.

Variables are introduced in declarations.

x: S The value of x belongs to the set S

y: S y is a set of S

i .. j - Number range: the set of numbers starting with i up through j

Elements of Z – Operations on Sets
13

5
Elements of Z – Operations on Sets
14
Combining Sets – Set Union

A B
 “A union B” is the set of all elements that are in
A, or B, or both.
 This is similar to the logical “or” operator.
Combining Sets – Set Intersection

A B
 “A intersect B” is the set of all elements that
are in both A and B.
 This is similar to the logical “and”
Set Complement

A
 “A complement,” or “not A” is the set of all
elements not in A.
 The complement operator is similar to the
logical not, and is reflexive, that is,

A A
Set Difference

𝐴\B
The set difference “A minus B” is the set of
elements that are in A, and not in B, so
𝐴\B = 𝐴 ∩ 𝐵

{1,2,3,4} \ {2,3} = {1,4}

{1,2,3,4} ∩ {2,3} = {1,2,3,4} ∩ {1,4} = {1, 4}
Universal set U

A  {1,2,3} B  {3,4,5,6}

A  B  {1,2,3,4,5,6} U = {1, 2, 3, 4, 5, 6}

𝐴 = {4,5,6} B  {1,2}

𝐵\𝐴 = 𝐵 ∩ 𝐴 = 3,4,5,6 ∩ {4,5,6} = {4,5,6}

 Elements of Z – Notation for Sets
20

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) is true

Example

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

The set of all squares of integer primes i.e. {1, 4, 9, 25 …}

 Elements of Z – Notation for Sets
21

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

Example

N = {x : Z | x ≥ 0}

The empty set

∅ = {x : T | false}

Note, in Z
∅ = ∅[T] is typed
Elements of Z – Predicates on Sets
22

Predicates are not expressions.

They do not have values, they can be true or false.
 Subset relationship

 Definition. Subset.

A B “A is a subset of B”

We say “A is a subset of B” if x  A  x  B
i.e., all the members of A are also members of
B. The notation for subset is very similar to
the notation for “less than or equal to,” and
means, in terms of the sets, “included in or
equal to.”
Proper Subset Relationship
 Definition. Proper Subset.

A B “A is a proper subset of B”
We say “A is a proper subset of B” if all the
members of A are also members of B, but in
addition there exists at least one element c such
that c  A but c  B

The notation for subset is very similar to the

notation for “less than,” and means, in terms of
the sets, “included in, but not equal to.”
Elements of Z – Predicates on Sets
25

For subset and proper subset relationships

S1 and S2 must have the same type

× Cartesian product
The Cartesian product of two sets A and B,
denoted by A × B is the set of all ordered
pairs (a, b) such that a is a member
of A and b is a member of B.
 Elements of Z – Arithmetic Operations
26

m+n Addition
m-n Subtraction
m*n Multiplication
m div n Division
m mod n Remainder (modulus)
m≤n Less than or equal
m .. n Number range
min A Minimum of a set of numbers
max A Maximum of a set of numbers
 Functions
27

A function is a correspondence between

two sets X and Y that assings to each
element x of set X exactly one element y
of Y .
Graphical Representations
 Functions can be represented graphically in
several ways:

f A B
• •
f • •
a• • • y
b •
•
• •
x
A Graph
B Plot
Like Venn diagrams
28
 Domain and Range
29

For each element x in X , the

corresponding element y in Y is called
the value of the function at x. The set X
is called the domain of the function, and
the set of all function values, Y , is called
the range of the function.
Determine, if a relation is a function

a. {(4,5), (6, 7), (8,8)}

b. {(5, 6), (4, 7), (6, 6), (6, 7)}

Solution We begin by making a figure

for each relation that shows set X , the
domain, and set Y , the range.
 Solution for part (a)

X Y The figure shows that every

4 5 element in the domain
6 7
8 8 corresponds to exactly one
element in the range.
Domain Range

This relation is a function

 Solution for part (b)

X Y
4 6 The figure shows that 6
5
6 7 corresponds to both 6 and 7.
Domain Range
If any element in the domain corresponds to
more than one element in the range, the
relation is not a function, Thus, the relation
is not a function.
Definition of a Function

Given any sets A, B, a function f from

(or “mapping”) A to B (f : AB) is an
assignment of exactly one element
f(x)B to each element xA.

33
 One-to-One Functions
34

 A function is one-to-one (1-1), or injective, iff

only one element of the domain is mapped
to any one element of the range.

• • • •
• • •
• • •
• • •
• •
• • • • •
• • •
• •
• •
Not one-to-one Not even a
One-to-one function!
34
 Elements of Z – Functions
35
 Elements of Z – pairs and binary relations
36
 Elements of Z – Logical Operations
37
 How to Model a System
 Z explicitly describes a system in terms of
mathematical types (set, sequences, relations,
functions) & user defined operations
 Z specification includes
• types – mathematical syntax of an object being specified
• invariants - properties of a modeled object
• operations – expressed in terms of pre/post conditions
 Z decomposes specifications into manageably sized
module’s, called schemas. Schemas have 3 parts:
 A State
 A collection of state variables and their values
 Operations that can change the state
Static and Dynamic Aspects of Behavior
39

 Static aspects
 The states that a system can occupy.
 The invariant relationships that are maintained as the
system moves from state to state.

 Dynamic aspects
 The possible operations.
 The relationship between their inputs and outputs.

 The changes of state that happen.

How to Specify Static Aspects?

Use schemas - math in a box with a name - to describe the

state space (state variables and invariants).

Name of schema

Declaration of state variables

Invariant relationship between values of the variables

The Birthday Book Example

 This specification will allow you to do 3 things:

 Add a person’s name and birthday
 Store that information
 Find a birthday by name
 Find a name by given date of birthday

 For example, lets define a state of the system, which

has three people in the set known, with their birthdays
recorded by the function birthday:
 Example: Birthday Book
42

 BirthdayBook schema for recording people’s birthdays

 [NAME; DATE] are basic types of the specification

 known: set of names

 birthday: function from names to birthdays

Q: What does the invariant say?

 Example: Birthday Book
 One possible state

 Stated properties
 No limit on the number of birthdays recorded
 No premature decision about the format of names and
dates
 Q: How many birthdays can a person have?
 Q: Does everyone have a birthday?
 Q: Can two persons share the same birthday?
43
How to Specify Dynamic Aspects?
 Define the schema of operation
 relationship between inputs (?) and outputs (!) of the
operation
 changes of the state that happen.

 Example: AddBirthday operation

 name? and date? are inputs
 birthday’ – is a next state of the book

44
 (Delta) And  (Xi) Notations
  BirthdayBook state change of BirthdayBook
  BirthdayBook no state change of BirthdayBook

45
 More operations: FindBirthday

 Use  notation
 No state change – we cannot use the prime ‘ symbol

46
More operations: Remind
 Use of set comprehension notation
 Selection | operation – “Such that”
 Q: What is the output of the Remind operation?

47
More Examples: InitBirthdayBook
 Describes the initial state of the system
 By convention, we use Init as a prefix

48
Proving Properties
 E.g., known’ = known  {name?}
50

Please ask your questions!