Z lecture notes: Schemas and Schema Calculus

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 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

$\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 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 =

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 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, ,

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}$

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

$\Delta$ Editor $\defs$ [ Editor; Editor' ]

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 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 (_ _) 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