% schema-slides.tex (root is schema.tex)


\pagestyle{empty}

\begin{slide}{}
SCHEMAS

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

\end{slide}

\begin{slide}{}
STATE SCHEMA

Simple text editor with limited memory.

\begin{zed}
	[CHAR]
\also
	TEXT == \seq CHAR
\end{zed} 

\begin{axdef}
	maxsize: \nat
\where
	maxsize \leq 65535
\end{axdef} 
The editor state is modelled by two {\em 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.

\begin{zed}Init \defs [~ Editor | left = right = \langle \rangle ~] \end{zed}

\end{slide}

\begin{slide}{}
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.

\end{slide}

\begin{slide}{}
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 {\em precondition} is the predicate that must be true for the
operation to be defined, involving only inputs and unprimed ``before''
variables.
$Forward$ is a {\em partial} operation. It does not 
cover the situation where the cursor is already at the end of the
buffer, $right = \langle \rangle$

\end{slide}

\begin{slide}{}
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.

\begin{zed}
        T\_Forward \defs Forward \\
\t2		\lor (EOF \land RightArrow \land \Xi Editor)
\end{zed} 
$T\_Forward$ is a {\em total} operation that is defined in all
$Editor$ states.

\end{slide}

\begin{slide}{}
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 {\em included} schema name (or {\em schema reference})
can be {\em 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}

\end{slide}


\begin{slide}{}
DECORATION, $\Delta$, $\Xi$

{\em 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.

\begin{zed}\Delta Editor \defs [~ Editor; Editor' ~] \end{zed}
$\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}

\end{slide}


\begin{slide}{}
SCHEMA CALCULUS

Merge declarations, combine predicates.

% To expand a {\em schema expression} merge declarations, combine
% predicates using the same logical connective used as the {\em schema
% operator}

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

\begin{zed} Division \defs Quotient \land Remainder \end{zed}
means the same as


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

\end{slide}

\begin{slide}{}
SCHEMA CALCULUS AND TOTAL OPERATIONS

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

\begin{zed}
	T\_Forward \defs Forward \\
\t2		\lor (EOF \land RightArrow \land \Xi Editor) 
\end{zed}
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 \\
\t1		\land left' = left \cat \langle head~right \rangle \\
\t1		\land right' = tail~right) \lor \\
	(right = \langle \rangle \land left' = left \land right' = right))
\end{schema}

\end{slide}

\begin{slide}{}
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:

\begin{tabbing}
xxxxxxxxxxx \= \kill \\ 
$S \semi T$ \> Schema composition \\
$S \pipe T$ \> Schema piping \\
\end{tabbing}

Composition is like relational composition and piping is like
conjunction, {\em not} sequencing.  

Z is not a programming language!


\end{slide}

\begin{slide}{}

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

\begin{zed} \forall Editor | Init @ EOF \end{zed}

This expands to an ordinary predicate.

\begin{zed}
\forall left, right: TEXT | \\
\t1	\# (left \cat right) \leq maxsize @ \\
\t2	left = right = \langle \rangle \implies right = \langle \rangle
\end{zed}

\end{slide}

\begin{slide}{}
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 % no parens needed
\where
	\dots
\end{axdef} 
The tool-kit provides this {\em generic definition}.

\begin{gendef}[X]
	\_ \cat \_ : \seq X \cross \seq X \fun \seq X
\where
	\dots
\end{gendef} 
$X$ is a {\em formal generic parameter} that can be {\em instantiated}
with an {\em actual generic parameter}.

Generic definitions can use patterns.

\begin{zed} X \rel Y == \power (X \cross Y) \end{zed}
Generic definitions can extend the Z notation.

\end{slide}

\begin{slide}{}
GENERIC SCHEMAS

{\em 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.

\end{slide}

\begin{slide}{}
FREE TYPES

Free types can model {\em 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$:

\begin{syntax}
	OP & ::= & plus | minus | times | divide 
\also
	EXP & ::= & const \ldata \nat \rdata \\
	    & | & binop \ldata OP \cross EXP \cross EXP \rdata
\end{syntax}

\end{slide}