The Origins of Z:
Jean-Raymond Abrial should lead the list of developers of the Z notation as he
started the beginnings of the notation.
Math Refresher:
N = {0,1,2,3,4,...}
Z = {...,-2,-1,0,1,2,...}
R = the set of all real numbers
Types and Sets:
(This was a point that was re-iterated by Gregory several times)
In the Z notation, types are sets, and sets are types.
Schema Calculus (not covered yet) is the most important type.
A type PERSON can be introduced by by the bracketing convention
[PERSON]
A variable of this type can be introduced as follows
jim : PERSON
jim is now a variable of type PERSON
Examples:
x : HOUSE | x is in New Orleans
x is of type HOUSE where x is in New Orleans
S == {x | x is not an element of x}
S is defined to be the set of all elements x such that x is not an element of x
S: seq X
S is a particular sequence of X
For example, if X = N, S can be {1,2}
Universal Quantification
'forall' is a universal quantifier
The step-by-step conversion of a statement from an informal language (English) to
a statement in formal language is shown below:
* at night, all cats are grey
* at night, for any c where c is an Animal, if c is a cat then c is grey
* it is night => forall c: ANIMAL . c is a cat => c is grey
(we need 'Animal' here because c needs to be type defined
But this can be expressed more concisely as
* it is night => forall c: CAT . c is grey
(Here, c is defined to be of TYPE CAT)
Power sets
P{} = {{}}
P{{}} = { {}, {{}} }
{} is the empty set
{{}} is the set that contains the empty set
{} != {{}}
Set Comprehension
This is a way of describing what the elements of the set are.
An expression of the form
{ variable : SET | predicate . term } translates to
Given that variable is of type SET, if predicate is true, return
term for all such values of variable over the range of SET.
In an expression of the form {variable : SET . term },
there is no predicate to be satisfied
For example, ( n : N . n ) is equivalent to N
(Exercise done in class):
Write a set comprehension denoting the set of all prime numbers
{ x : Z+ | x != 1 AND x is prime }
Pairs and Comprehension
S * T = { a:S ; b:T }
T * S = { b:T ; a:S }
In this case, S*T == T*S because both sets have the same elements although in different order.
But in general, S*T != T*S
Therefore, a clearer way of producing the above set is:
S*T= { a:S; b:T . (a,b) } = { b:T; a:S . (a,b) } = T*S
Type Definitions
When introducing types,
[ N, Z, R ] is equivalent to
[ N ]
[ Z ]
[ R ]
Abbreviation definition
symbol == term
introduces a new global constant symbol with the same type and value as
expression term
For example, Coordinate == N * N
introduces Coordinate as a global constant which is of type
'Ordered pair of two natural numbers'.
Suppose we define evens as
evens == {n: N | 2 divides n },
we can simply introduce x as x:evens
We do not need to declare x:N before and then observe that x is an element
of evens
However, we cannot simply declare 'x is an element of evens' by itself as x
would not be type-defined yet.
Generic Definitions
Let's go through an example we did in class)
_______[X]_____________________________________________________________
_______________________________________________________________________
| _ subset-of _ : PX <-> PX
|_______________________
| Forall S,T : PX .
S subset-of T <=> forall x : X . x element-of S => x element-of T
|_______________________________________________________________________
This is a generic definition for the subset operation
Thus, we define the subset relationship on type X where we don't really care what X is.
The only constraints are that the two arguments are power sets of X.
The two blanks in the first line are replaced by the arguments S and T in that order.