SCHEMAS AND SCHEMA CALCULUS

Based on chapters 12 and 14 in The Way of Z.

Links to more Z lectures.

This page looks best when this \power and this X are about the same size: \power 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

\begin{axdef}
maxsize: \nat
\where
maxsize \leq 65535
\end{axdef}

The editor state is modelled by two state variables, the texts to the left and right of the cursor.

\begin{schema}{ Editor }

left, right: TEXT
\where
# (left \cat right) \leq maxsize
\end{schema}

The editor starts up empty.

Init \defs [  Editor | left = right = \langle \rangle  ]

OPERATION SCHEMA

The Insert operation inserts a printing character to the left of the cursor.

\begin{axdef}
printing: \power CHAR
\end{axdef}

\begin{schema}{ Insert }

\Delta Editor
ch?: CHAR
\where
ch? \in printing
left' = left \cat \langle ch? \rangle
right' = right
\end{schema}

Delta in \Delta 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.

\begin{axdef}
right_arrow: CHAR
\where
right_arrow \notin printing
\end{axdef}

\begin{schema}{ Forward }

\Delta Editor
ch?: CHAR
\where
ch? = right_arrow
right \neq \langle \rangle
left' = left \cat \langle head(right) \rangle
right' = tail(right)
\end{schema}

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 = \langle \rangle


SCHEMA CALCULUS, TOTAL OPERATIONS

In EOF states the cursor is at end-of-file.

\begin{schema}{ EOF }

Editor
\where
right = \langle \rangle
\end{schema}

Box up right_arrow for schema expressions.

\begin{schema}{ RightArrow }

ch?: CHAR
\where
ch? = right_arrow
\end{schema}

Xi in \Xi Editor indicates no change in state.

T_Forward \defs Forward \lor (EOF \land RightArrow \land \Xi Editor)

T_Forward is a total operation that is defined in all Editor states.


SCHEMA INCLUSION, EXPANSION

Schemas can be used like macros.

\begin{schema}{ Editor }

left, right: TEXT
\where
# (left \cat right) \leq maxsize
\end{schema}

\begin{schema}{ Init }

Editor
\where
left = right = \langle \rangle
\end{schema}

Any included schema name (or schema reference) can be expanded by replacing the name by the text.

\begin{schema}{ Init }

left, right: TEXT
\where
# (left \cat right) \leq maxsize
left = right = \langle \rangle
\end{schema}

DECORATION, \Delta, \Xi

Decorations give identifiers conventional meanings (prime ' indicates ``after''). Decorating a schema name decorates all its state variables.

\begin{schema}{ Editor' }

left', right': TEXT
\where
# (left' \cat right') \leq maxsize
\end{schema}

\Delta indicates the operation schema that includes the before state and the after state.

\Delta Editor \defs [  Editor; Editor'  ]

\Xi indicates the operation where before and after states are the same.

\begin{schema}{ \Xi Editor }

\Delta Editor
\where
left' = left
right' = right
\end{schema}

SCHEMA CALCULUS

Merge declarations, combine predicates.

\begin{schema}{ Quotient }

n, d, q, r: \nat
\where
d \neq 0
n = q*d + r
\end{schema}

\begin{schema}{ Remainder }

r, d: \nat
\where
r < d
\end{schema}

Division \defs Quotient \land Remainder

means the same as

\begin{schema}{ Division }

n,d,q,r: \nat
\where
d \neq 0
r < d
n = q*d + r
\end{schema}

SCHEMA CALCULUS AND TOTAL OPERATIONS

Any schema expression can be expressed as a single schema box.

T_Forward \defs Forward
    \lor (EOF \land RightArrow \land \Xi Editor)

means the same as

\begin{schema}{ T_Forward }

left, right, left', right': TEXT
ch?: CHAR
\where
# (left \cat right) \leq maxsize
# (left' \cat right') \leq maxsize
ch? = right_arrow
((right \neq \langle \rangle
    \land left' = left \cat \langle head right \rangle
    \land right' = tail right) \lor
(right = \langle \rangle \land left' = left \land right' = right))
\end{schema}

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 \semi T     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''

\forall Editor | Init @ EOF

This expands to an ordinary predicate.

\forall left, right: TEXT | # (left \cat right) \leq maxsize @
    left = right = \langle \rangle \implies right = \langle \rangle

GENERIC DEFINITIONS

A definition of sequence concatenation (_ \cat _) that applied to only one type would not be very useful.

\begin{axdef}
_ \cat _ : TEXT \cross TEXT \fun TEXT
\where
...
\end{axdef}

The tool-kit provides this generic definition.

\begin{gendef} [X]

_ \cat _ : seq X \cross seq X \fun seq X
\where
...
\end{gendef}

X is a formal generic parameter that can be instantiated with an actual generic parameter.

Generic definitions can use patterns.

X \rel Y == \power (X \cross Y)

Generic definitions can extend the Z notation.


GENERIC SCHEMAS

Generic schemas have type parameters.

\begin{schema}{ Pool[RESOURCE] }

owner: RESOURCE \pfun USER
free: \power RESOURCE
\where
(dom owner) \cup free = RESOURCE
(dom owner) \cap free = \emptyset
\end{schema}

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 \ldata \nat \rdata | binop \ldata OP \cross EXP \cross EXP \rdata

Back to Z lectures.


Jonathan Jacky / University of Washington / Seattle, Washington / USA
E-mail: jon@u.washington.edu