Based on chapters 12 and 14 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.
Schema: math in a box, with a name attached.
Unique to Z.
Schema calculus builds large schemas from smaller ones.
Model states and operations.
Can be used as declarations, predicates, expressions, types, sets ...
STATE SCHEMA
Simple text editor with limited memory.
[CHAR] |
![]() |
TEXT == seq CHAR |
![]() | ||
maxsize: ![]() | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
maxsize ![]() | ||
![]() |
The editor state is modelled by two state variables, the texts to the left and right of the cursor.
![]() |
Editor | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
left, right: TEXT | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
# (left ![]() ![]() | |||
![]() | |||
![]() |
The editor starts up empty.
Init ![]() ![]() ![]() |
OPERATION SCHEMA
The Insert operation inserts a printing character to the left of the cursor.
![]() | ||
printing: ![]() | ||
![]() |
![]() |
Insert | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
![]() | |||
ch?: CHAR | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
ch? ![]() | |||
left' = left ![]() ![]() ![]() | |||
right' = right | |||
![]() | |||
![]() |
Delta in Editor indicates state change.
Unprimed left, primed left' represent before and after.
Question mark ch? indicates input.
PRECONDITIONS, PARTIAL OPERATIONS
The Forward operation moves the cursor forward.
![]() | ||
right_arrow: CHAR | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
right_arrow ![]() | ||
![]() |
![]() |
Forward | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
![]() | |||
ch?: CHAR | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
ch? = right_arrow | |||
right ![]() ![]() ![]() | |||
left' = left ![]() ![]() ![]() | |||
right' = tail(right) | |||
![]() | |||
![]() |
The precondition is the predicate that must be true for the
operation to be defined, involving only inputs and unprimed ``before''
variables.
Forward is a partial operation. It does not
cover the situation where the cursor is already at the end of the
buffer, right =
SCHEMA CALCULUS, TOTAL OPERATIONS
In EOF states the cursor is at end-of-file.
![]() |
EOF | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
Editor | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
right = ![]() ![]() | |||
![]() | |||
![]() |
Box up right_arrow for schema expressions.
![]() |
RightArrow | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
ch?: CHAR | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
ch? = right_arrow | |||
![]() | |||
![]() |
Xi in Editor indicates no change in state.
T_Forward ![]() ![]() ![]() ![]() ![]() |
T_Forward is a total operation that is defined in all Editor states.
SCHEMA INCLUSION, EXPANSION
Schemas can be used like macros.
![]() |
Editor | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
left, right: TEXT | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
# (left ![]() ![]() | |||
![]() | |||
![]() |
![]() |
Init | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
Editor | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
left = right = ![]() ![]() | |||
![]() | |||
![]() |
Any included schema name (or schema reference) can be expanded by replacing the name by the text.
![]() |
Init | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
left, right: TEXT | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
# (left ![]() ![]() | |||
left = right = ![]() ![]() | |||
![]() | |||
![]() |
DECORATION, ,
Decorations give identifiers conventional meanings (prime ' indicates ``after''). Decorating a schema name decorates all its state variables.
![]() |
Editor' | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
left', right': TEXT | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
# (left' ![]() ![]() | |||
![]() | |||
![]() |
indicates the operation schema that includes the
before state and the after state.
![]() ![]() |
indicates the operation where before and after states are the
same.
![]() |
![]() |
![]() | |
![]() |
![]() |
![]() | |
![]() | |||
![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
left' = left | |||
right' = right | |||
![]() | |||
![]() |
SCHEMA CALCULUS
Merge declarations, combine predicates.
![]() |
Quotient | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
n, d, q, r: ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
d ![]() | |||
n = q*d + r | |||
![]() | |||
![]() |
![]() |
Remainder | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
r, d: ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
r < d | |||
![]() | |||
![]() |
Division ![]() ![]() |
means the same as
![]() |
Division | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
n,d,q,r: ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
d ![]() | |||
r < d | |||
n = q*d + r | |||
![]() | |||
![]() |
SCHEMA CALCULUS AND TOTAL OPERATIONS
Any schema expression can be expressed as a single schema box.
T_Forward ![]() |
![]() ![]() ![]() ![]() ![]() |
means the same as
![]() |
T_Forward | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
left, right, left', right': TEXT | |||
ch?: CHAR | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
# (left ![]() ![]() | |||
# (left' ![]() ![]() | |||
ch? = right_arrow | |||
((right ![]() ![]() ![]() | |||
![]() ![]() ![]() ![]() ![]() | |||
![]() ![]() ![]() | |||
(right = ![]() ![]() ![]() ![]() | |||
![]() | |||
![]() |
OTHER SCHEMA CALCULUS OPERATORS
There is a schema operator for every logical connective and quantifier.
Conjunction and disjunction are most useful.
Schema negation is uninituitive, not very useful.
Two operators are not based on logical connectives:
S ![]() | Schema composition |
S >> T | Schema piping |
Composition is like relational composition and piping is like conjunction, not sequencing.
Z is not a programming language!
SCHEMAS AS DECLARATIONS, PREDICATES
Schemas can be used like macros to write compact formulas.
``When an editor is in its initial state, the cursor is at the end of the file''
![]() ![]() |
This expands to an ordinary predicate.
![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() |
GENERIC DEFINITIONS
A definition of sequence concatenation (_ _) that applied to
only one type would not be very useful.
![]() | ||
_ ![]() ![]() ![]() | ||
![]() | ||
![]() |
![]() |
![]() |
![]() | ||
... | ||
![]() |
The tool-kit provides this generic definition.
![]() |
[X] | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
_ ![]() ![]() ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
... | |||
![]() | |||
![]() |
X is a formal generic parameter that can be instantiated with an actual generic parameter.
Generic definitions can use patterns.
X ![]() ![]() ![]() |
Generic definitions can extend the Z notation.
GENERIC SCHEMAS
Generic schemas have type parameters.
![]() |
Pool[RESOURCE] | ![]() | |
![]() |
![]() |
![]() | |
![]() | |||
owner: RESOURCE ![]() | |||
free: ![]() | |||
![]() | |||
![]() |
![]() |
![]() | |
![]() | |||
(dom owner) ![]() | |||
(dom owner) ![]() ![]() | |||
![]() | |||
![]() |
RESOURCE could be instantiated with different types for memory pages, disk blocks, etc.
FREE TYPES
Free types can model recursive data types used to build linked structures.
Example: define syntax of simple arithmetic expressions on natural numbers, such as 2+3 and (12 div (2+3)) - 7:
OP ::= plus | minus | times | divide |
EXP ::= const ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Back to Z lectures.