### SCHEMAS AND SCHEMA CALCULUS

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

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 65535

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

 Editor left, right: TEXT # (left right) maxsize

The editor starts up empty.

 Init [  Editor | left = right =  ]

OPERATION SCHEMA

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

 printing: CHAR

 Insert Editor ch?: CHAR ch? printing left' = left ch? 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 printing

 Forward Editor ch?: CHAR ch? = right_arrow right left' = left head(right) 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 Forward (EOF RightArrow Editor)

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 right) maxsize

 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 right) maxsize 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' right') maxsize

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

 Editor [  Editor; Editor'  ]

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

 Editor Editor left' = left right' = right

SCHEMA CALCULUS

Merge declarations, combine predicates.

 Quotient n, d, q, r: d 0 n = q*d + r

 Remainder r, d: r < d

 Division Quotient Remainder

means the same as

 Division n,d,q,r: d 0 r < d n = q*d + r

SCHEMA CALCULUS AND TOTAL OPERATIONS

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

 T_Forward Forward (EOF RightArrow Editor)

means the same as

 T_Forward left, right, left', right': TEXT ch?: CHAR # (left right) maxsize # (left' right') maxsize ch? = right_arrow ((right left' = left head right right' = tail right) (right = left' = left 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 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''

 Editor | Init EOF

This expands to an ordinary predicate.

 left, right: TEXT | # (left right) maxsize left = right = right =

GENERIC DEFINITIONS

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

 _ _ : TEXT TEXT TEXT ...

The tool-kit provides this generic definition.

 [X] _ _ : seq X seq X seq X ...

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

Generic definitions can use patterns.

 X Y == (X Y)

Generic definitions can extend the Z notation.

GENERIC SCHEMAS

Generic schemas have type parameters.

 Pool[RESOURCE] owner: RESOURCE USER free: RESOURCE (dom owner) free = RESOURCE (dom owner) free =

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 | binop OP EXP EXP

Back to Z lectures.

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