SCHEMA TYPES AND BINDINGS

Based on chapter 13 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.

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, \power X, instances are sets.

Cartesian product types, X \cross Y, instances are tuples.

Schema types, \lblot x: X; y: Y \rblot, 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 \cross MONTH \cross YEAR

Instances of DATE are tuples.

\begin{axdef}
landing, opening: DATE
\where
landing = (20, 7, 1969)
opening = (9, 11, 1989)
\end{axdef}

But nothing prevents tuples that indicate impossible dates.

\begin{axdef}
d: DATE
\where
d = (29, 2, 1997)
\end{axdef}

Cartesian product types cannot express constraints between components.

SCHEMA TYPES

Can express contraints between components.

days == \langle 31, 28, 31, 30, 31, 30, ..., 30, 31 \rangle

\begin{schema}{ TypicalDate }

day: 1 .. 31
month: 1 .. 12
year: \num
\where
day \leq days month
\end{schema}

(leap _) == {  y: \num @ 4*y  } \ ({  y: \num @ 100*y  } \ {  y: \num @ 400*y  })

\begin{schema}{ Feb29 }

month, day, year: \num
\where
month = 2
day = 29
leap year
\end{schema}

Date \defs TypicalDate \lor Feb29

SCHEMA TYPE SIGNATURE

The schema type is determined by the signature: names and types (but not the order) of state variables.

\begin{schema}{ TypicalDate }

day: 1 .. 31
month: 1 .. 12
year: \num
\where
day \leq days month
\end{schema}

The signature is visible after normalizing.

\begin{schema}{ TypicalDate }

day, month,year: \num
\where
day \in 1 .. 31
month \in 1 .. 12
day \leq days month
\end{schema}

The schema type is \lblot day, month, year: \num \rblot.

USING SCHEMA TYPES

Schema references can appear in declarations. The selector dot indicates particular state variables.

\begin{axdef}
landing: Date
\where
landing.day = 20
landing.month = 7
landing.year = 1969
\end{axdef}

or

\begin{schema}{ MultiEditor }

active: NAME
buffer: NAME \pfun Editor
\where
active \in dom buffer
\end{schema}

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.

\begin{axdef}
landing: \lblot day, month, year:\num \rblot
\where
landing = \langle day :> 20, month :> 7, year :> 1969 \rangle
\end{axdef}

This alternative must be used instead.

\begin{axdef}
landing: Date
\where
landing.day = 20
landing.month = 7
landing.year = 1969
\end{axdef}

BINDING FORMATION OPERATOR, \theta

\theta S (theta S) is the (nameless) instance of schema type S which is in scope. Instead of

\begin{axdef}
weekday: Date \fun 0 .. 6
\where
\forall d: Date @ weekday(d) = (d.day + ...) mod 7
\end{axdef}

we can write

\begin{axdef}
weekday: Date \fun 0 .. 6
\where
\forall Date @ weekday(\theta Date) = (day + ...) mod 7
\end{axdef}

Instead of

\begin{schema}{ \Xi Editor }

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

we can write

\Xi Editor \defs [  \Delta Editor | \theta Editor' = \theta Editor ]

SCHEMAS AS RELATIONS

We can use \theta to define the binary relation corresponding to an operation schema.

\begin{schema}{ Precedes }

\Delta Date
\where
(year < year') \lor
(year = year' \land month < month') \lor
(year = year' \land month = month' \land day < day')
\end{schema}

precedes == {  Precedes @ (\theta Date, \theta Date')  }

Now precedes is a binary relation on Date.

\begin{schema}{ Biography }

name: NAME
birth, death: Date
...
\where
birth precedes death
...
\end{schema}

Back to Z lectures.

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