Based on chapter 13 in The Way of Z.
Links to more Z lectures.
This page looks best when this and this X are
about the same size:
X. See these viewing tips.
A schema defines a new type whose instances are record-like objects called bindings.
There are only four kinds of data types in Z.
Basic types, [X], instances are individuals.
Set types, X, instances are sets.
Cartesian product types, X Y, instances are tuples.
Schema types, x: X; y: Y
, instances are bindings.
Schema types and bindings enable Z to model large systems and support an object-oriented style.
CARTESIAN PRODUCT TYPES
Declare the Cartesian product type DATE.
DATE == DAY ![]() ![]() |
Instances of DATE are tuples.
![]() | ||
landing, opening: DATE | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
landing = (20, 7, 1969) | ||
opening = (9, 11, 1989) | ||
![]() |
But nothing prevents tuples that indicate impossible dates.
![]() | ||
d: DATE | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
d = (29, 2, 1997) | ||
![]() |
Cartesian product types cannot express constraints between components.
SCHEMA TYPES
Can express contraints between components.
days == ![]() ![]() |
![]() |
TypicalDate | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
day: 1 .. 31 | |||
month: 1 .. 12 | |||
year: ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
day ![]() | |||
![]() | |||
![]() |
(leap _) == { y: ![]() ![]() ![]() ![]() ![]() ![]() |
![]() |
Feb29 | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
month, day, year: ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
month = 2 | |||
day = 29 | |||
leap year | |||
![]() | |||
![]() |
Date ![]() ![]() |
SCHEMA TYPE SIGNATURE
The schema type is determined by the signature: names and types (but not the order) of state variables.
![]() |
TypicalDate | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
day: 1 .. 31 | |||
month: 1 .. 12 | |||
year: ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
day ![]() | |||
![]() | |||
![]() |
The signature is visible after normalizing.
![]() |
TypicalDate | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
day, month,year: ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
day ![]() | |||
month ![]() | |||
day ![]() | |||
![]() | |||
![]() |
The schema type is day, month, year:
.
USING SCHEMA TYPES
Schema references can appear in declarations. The selector dot indicates particular state variables.
![]() | ||
landing: Date | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
landing.day = 20 | ||
landing.month = 7 | ||
landing.year = 1969 | ||
![]() |
or
![]() |
MultiEditor | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
active: NAME | |||
buffer: NAME ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
active ![]() | |||
![]() | |||
![]() |
Schema references can be used as set valued expressions.
SCHEMA TYPE NOTATION
According to The Z Notation: A Reference Manual (ZRM), the notation for schema types and bindings is not part of Z itself.
This is not Z, according to the ZRM.
![]() | ||
landing: ![]() ![]() ![]() | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
landing = ![]() ![]() | ||
![]() |
This alternative must be used instead.
![]() | ||
landing: Date | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
landing.day = 20 | ||
landing.month = 7 | ||
landing.year = 1969 | ||
![]() |
BINDING FORMATION OPERATOR,
S (theta S) is the (nameless) instance of schema type
S which is in scope. Instead of
![]() | ||
weekday: Date ![]() | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
![]() ![]() | ||
![]() |
we can write
![]() | ||
weekday: Date ![]() | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
![]() ![]() ![]() | ||
![]() |
Instead of
![]() |
![]() |
![]() | |
![]() |
![]() |
![]() | |
![]() | |||
![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
left' = left | |||
right' = right | |||
![]() | |||
![]() |
we can write
![]() ![]() ![]() ![]() ![]() |
SCHEMAS AS RELATIONS
We can use to define the binary relation
corresponding to an operation schema.
![]() |
Precedes | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
(year < year') ![]() | |||
(year = year' ![]() ![]() | |||
(year = year' ![]() ![]() | |||
![]() | |||
![]() |
precedes == { Precedes ![]() ![]() ![]() |
Now precedes is a binary relation on Date.
![]() |
Biography | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
name: NAME | |||
birth, death: Date | |||
... | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
birth precedes death | |||
... | |||
![]() | |||
![]() |
Back to Z lectures.