The characteristic features of Z are:
- it is based upon set theory and mathematical logic;
- the schemas are used to describe the states of systems, and the ways in which the states may change;
- it is a typed language (every object has a type);
- the natural language is used to relate the chosen objects to the real world, by choosing the suitable meaningful names for variables, and to give additional information through comments;
- we may refine a description of a system by constructing another model closer to implementation.
Definitions
The following notation is used to define a symbol:
Symbol = = content (or meaning)
Example:
Rcolour = = {red, yellow, blue } ∈ ℙ Colours
Declarations
[Guest, Room] states that Guest and Room are two types, the set of all guests, and the set of all rooms, respectively.
x : Guest declares a variable x of type Guest
Generic abbreviations
∅[T] = = {x∈T | false} is the empty set of objects of type T
ℙ 1 T = = {m ∈ ℙT | m ≠ ∅[T] }
s rel t = = ℙ(s × t)
r ∈ s rel t is a relation between s and t
Axiomatic definitions
|__declaration __
| predicate
|__x ∈ S __
| p
here p is a constraint on the elements of S
|__N : ℙ ℤ __
| ∀z : ℤ • z∈N⇔ z≥0
Generic definitions
┍==[X] ====================
│ x : X
├────────────────────────
│ p
└─────────────────
introduces a generic constant x of type X satisfying predicate p.
Sets and predicates
The set C = {x:T | p(x) } is called the characteristic set of p.
Relations
By X ↔ Y = = ℙ (X × Y) we denote the set of all relations between X and Y.
If R ∈ X ↔ Y then
dom R = = {x:X | ∃y∈Y, (x,y) ∈R}
ran R = = {y:Y | ∃x∈X, (x,y) ∈R}
X is the source of R and Y is the target of R.
Types
Type = a set of values !
Examples: ℕ, ℤ, ℙT, T1 × T2, 1..n
Colours = = red | orange | yellow | green | blue | indigo | violet
nat = = zero | succ(nat)
Schemas
A schema consists of two parts:
- a declaration of variables;
- a predicate constraining their values.
We may write a schema in the following two ways:
[ declaration | predicate ]
or
Example: A concert hall uses a software system to keep track of bookings for performances. The system needs the sets of seats and customers, denoted by Seat, and Customer, respectively. The set seating ⊂ Seat represents the seating allocated for the performance (not all seats must be sold).
We can give a name to this schema in the following way:
===BoxOffice=================
A schema may be used to define a type. For example:
===SchemaOne===============
where Zile = = 1..31
defines a composite type with two components: an integer called Luna, and a subset of Zile, called ZileLucrate. The declaration p : SchemaOne introduces an object of schema type SchemaOne.
A date is an object consisting of two components: the name of a month and the number of a day. We need the set of months:
Month = = jan | feb | mar | apr | may | jun | jul | aug | sep | oct | nov | dec
===Date====================
These schema types difer from a cartesian product in that the components are stored not by position but by name. To select a component we employ the selection operator -.-. For p : TypeOne
we can have p.Luna and p.Salar. For JohnBirthday : Date
te components are JohnBirthdate.month and JohnBirthdate.day .
As another example, we mention that in an Ethernet network, information is transmitted in the form of data frames. Each frame has a source address, a destination, and a data component. The type of all frames is a schema type:
===Frame====================
Schemas as declarations
We may use a schema to define a new one, with the same components, but under some constraints. For example, the schema
===SchemaTwo===============
describes a subset of SchemaOne, with the property Luna≤6 and ZileLucrate is not empty. The same efect could be achieved by replacing SchemaTwo with a list of declarations and a constraint:
{ Luna : 1..12; ZileLucrate : ℙ Zile | Luna≤6∧ ZileLucrate ≠ Ø ● (Luna,ZileLucrate)}
The set comprehension {Date | day = 31 ● month} describes the set of all months that have 31 days, i.e. {jan, mar, may, jul, aug, oct, dec}
Schemas as predicates
If A is an element of type Address, the set of all addresses within a network, then the following schema represents the set of all frames whose source address is A:
===FrameA==================
Used as a predicate, this schema asserts that the value of source is A.
Renaming
It is sometimes useful to rename the components of a schema. If S is a schema, then we write S(new/old) to denote the schema obtained from S by replacing component name old with new.
For example SchemaTwo(StartL/Luna, ZileC/ZileLucrate) is equivalent to the schema
Generic Schemas
If we wish to use the same structure for a variety of diferent types, we may define a generic schema, i.e. a schema with one ore more formal parameters.
For example, if
===SchemaZ[T1,T2] ==========
then SchemaTwo is equivalent to SchemaZ[1..12/T1, Zile/T2].
Characteristic binding
To write an object of schema type in extension, we list the component names and the values to which they are bound. For this we need a notation to bind a variable of some values. For example, for schema SchemaOne through
Luna ⇝ 2, ZileLucrate ⇝ {1, 2, 4, 8}
Luna is bound to 2, and Zile lucrate is bound to {1, 2, 4, 8}.
Through a ⇝ a, b ⇝ b
(the left b is a component name, and the right b is a variable value) we denote a binding in which the component a is bound to the value of variable a, and compolnent b is bound to the value of variable b. Such a binding, in which each component of a schema is bound to a value of the same name, is called a characteristic binding.
If S is the name of a schema then we write θS to denote the characteristic binding of components from S.
References
1. Soo Dong Kim, Formal Specification in OO Software Development, PhD Thesis, 1991, Iowa University
2. Jim Woodcock, Jim Davies, Using Z: Specification, Refinement, and Proof
Univ. of Oxford Univ. of Oxford
