% Z example specification
% For 2/CS/3T Z course, October 1999
% Pro forma by Jonathan Bowen

% Based on Exercise 4 - but add error reports too.


\documentclass[11pt,fleqn]{article}

% The "oz" Z style file:
\usepackage{oz}
% The "ZTC" extra commands:
\usepackage{ztc}
% Nice PostScript fonts:
\usepackage{pslatex}
% A4 page size:
\usepackage{a4}

% Don't produce extra files like ".aux" - not needed here.
\nofiles

% The following causes paragraphs to be un-indented.
\parskip=1ex
\parindent=0ex
% Otherwise \noindent prevents paragraphs being indented if required.


\title{PUT YOUR TITLE HERE (2/CS/3T)}
\author{PUT YOUR NAME HERE}
\date{PUT THE DATE HERE}

\let\empty\emptyset

\begin{document}

\maketitle

\begin{abstract}
PUT A BRIEF DESCRIPTION HERE
\end{abstract}


% Sections:
\section{Introduction}

Note you can do the following using \LaTeX:

\begin{itemize}

\item
{\em Emphasized (italic) text}

\item
{\bf Bold text}

\item
{\tt Teletype (fixed font width) text}

\item
Math mode, e.g., $f? \in files$ if you want to put any Z names,
etc., in paragraphs

\item
``double quotes'' and `single quotes' are possible, but use
back-quotes for the lead quotation marks in \LaTeX

\end{itemize}

Note you can also have sections using \\
\verb"\section{"\ldots\verb"}" and subsections using \\
\verb"\subsection{"\ldots\verb"}".
You can force new lines using \verb"\\".

Paragraphs are delimited by blank lines.

\verb"--" gives a long dash (--),
\verb"---" gives a very long dash (---).

The rest of this file includes the start of a Z specification
with comment son what is required. Try to update this file with
a specification along the lines of that required for Exercise 4
in the course notes. If you get stuck, look at the answers!
Use the ZTC manual in the course notes for information on ZTC
mark-up.

Comment lines start with a \verb"%".
You can delete or comment out the information above once you have
read it!


\subsection{Basic sets}

INTRODUCE THE BASIC SETS:

\begin{zed}
[File,Printer]
\end{zed}


\subsection{Error messages}

INTRODUCE THE DIFFERENT TYPES OF ERROR:

\begin{zed}
  Report ::= Success\_Rep | File\_Exists\_Rep | Printing\_File\_Rep
\end{zed}

ADD MORE ERROR REPORTS IF NECESSARY


\section{Abstract state}

DESCRIBE THE ABSTRACT STATE

% This will help ZANS (Don't delete!):
%% state-schema System

\begin{schema}{System}
  file, printfiles : \power File \\
  printers : \power Printer \\
  printing\_on : File \rel Printer
\where
  \mbox{ADD THE PREDICATES HERE}
\end{schema}

Delete the {\em whole} line in the predicate part of the schema
above. Note that there is an error in the declarations compared
to Exercise 4.

(YOU MAY SUBSEQUENTLY ADD TO OR MODIFY THIS STATE IF YOU WISH)


\subsection{Initial state}

DESCRIBE THE INITIAL STATE

% This will help ZANS (Don't delete!):
%% init-schema InitSystem

\begin{schema}{InitSystem}
  System'
\where
  \mbox{ADD THE PREDICATE(S) HERE}
\end{schema}

(REMEMBER TO THINK ABOUT ALL THE STATE COMPONENTS)


\subsection{Change of state}

DESCRIBE THE GENERAL CHANGE OF STATE

\begin{schema}{\Delta System}
  System \\
  System'
\where
  \mbox{INVARIANTS IF ANY}
\end{schema}


\subsection{No change of state}

DESCRIBE NO CHANGE OF STATE

\begin{schema}{\Xi System}
  \Delta System
\where
  \theta System' = \theta System
\end{schema}

(THIS IS THE DEFAULT DEFINITION)


\section{Successful operations}

\begin{schema}{NewFile}
  \Delta System \\
  f? : File
\where
  \mbox{ADD PRECONDITION(S)} \\
  \mbox{ADD POSTCONDITIONS FOR ALL AFTER-STATE COMPONENTS}
\end{schema}

\begin{schema}{RemoveFile}
  \mbox{ADD DECLARATIONS AND PREDICATES}
\end{schema}


TRY ADDING A STATUS OPERATION THAT RETURNS THE FILES CURRENTLY
BEING PRINTED AS AN OUTPUT AND LEAVES THE STATE THE SAME


ADD MORE OF YOUR OWN OPERATIONS HERE IF YOU WISH \\
E.G.: REQUEST A FILE TO BE PRINTED ON A PRINTER



\section{Errors}

DESCRIBE THE SUCCESSFUL CASE BRIEFLY:

\begin{schema}{Success}
  rep! : Report
\where
  rep! = Success\_Rep
\end{schema}


DESCRIBE THE FOLLOWING ERROR SCHEMA

\begin{schema}{FileExists}
  \Xi System \\
  f? : File
  rep! : Report
\where
  \mbox{ADD PRECONDITION -- NEGATION OF SUCCESSFUL OPERATION} \\
  rep! = \mbox{ADD ERROR REPORT}
\end{schema}

ADD MORE ERROR SCHEMAS HERE AS REQUIRED


\subsection{Total operations}

DESCRIBE THE TOTAL OPERATIONS

% This will help ZANS (Don't delete!):
% (Add similar entries for other total operations in due course)
%% operation AddFile

\begin{zed}
  AddFile \defs (NewFile \land Success) \lor FileExists
\also
  \mbox{ADD MORE TOTAL OPERATIONS}
\end{zed}

TRY TO TYPE-CHECK, LATEX AND VIEW THIS FILE ONCE YOU HAVE EDITED IT:

\begin{quote}
\begin{verbatim}
  ztc exercise.tex -T
  latex exercise
  xdvi exercise &
\end{verbatim}
\end{quote}

There will be lots of errors at the moment because of the inclusion of
comments in schemas. You will need to edit these out as you amend this
file. The \verb"-T" option for \verb"ztc" creates a file called
\verb"exercise.typ" in the example above that contains Z type
information as determined by \verb"ztc".

``\verb"dvips -Plw exercise"'' (for example) should print the
\verb"exercise.dvi" file (produced by \LaTeX) when you have finished
(on the \verb"lw" printer in this example) if you wish to keep a
printed record of you specification.

You can edit or comment out this too once you have done it!

\end{document}