Relay-Version: version B 2.10.2 9/18/84 +2.11; site uk.ac.ox.prgv Posting-Version: version B 2.10.3 uknet 86/05/14; site uk.ac.oxford.prg Path: prgv!mkhadmin From: Ruaridh Macdonald (on UK.MOD.RSRE) Newsgroups: zforum Subject: Z Forum Issue 4.3 Message-ID: <16 MAY 1989 13:37:21 RM@RSRE> Date: 16 May 89 13:49:44 GMT Date-Received: 16 May 89 13:51:46 GMT Lines: 1502 21st April 1989 Z FORUM Volume 4 Issue 3 --------------- ------- ---------------- Today's Topics -------------- Bibliography Addendum Z Users Meeting Proceedings --------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Fri, 21 Apr 89 15:07 Subject: Bibliography Addendum %A D.H. Kemp %T Specification of Viper1 in Z %R RSRE Memorandum No. 4195 %I Royal Signals and Radar Establishment, MoD, UK %P 33 %D October 1988 %A D.H. Kemp %T Specification of Viper2 in Z %R RSRE Memorandum No. 4217 %I Royal Signals and Radar Establishment, MoD, UK %P 64 %D October 1988 ---------------------------------------------------------------------- Date: Thu, 13 Apr 89 15:57:10 BST From: Jonathan Bowen Subject: Z Users Meeting Proceedings Here finally is the Z Users Meeting Proceedings in LaTeX source form. As well as LaTeX you will need the "fuzz" or "zed" style option to format it properly. A printed copy, together with posters and other related papers, will be sent to all delegates at the meeting in the not too distant future. My apologies for the late appearance of the Proceedings. The next meeting is set for Friday 15th December 1989. The Proceedings, other Z related files and back issues of Z FORUM are available on the PRG archive server. For example, the following commands may be sent to (JANET) or (UUCP): help - send help on using the archive server index - master index of categories index z - index of Z related files send z 4.2 - send issue 4.2 of Z FORUM send z proc88.tex - send the Proceedings below -- Jonathan Bowen Programming Research Group Oxford University ------------------------ snip snip -------------------------- % Proceedings of Z Users Meeting, Oxford, 16th December 1988. % Compiled by Jonathan Bowen, Programming Research Group, Oxford University. \def\crest{} \documentstyle[11pt,twoside,fuzz,crest,pounds]{article} % Style options: % 11pt - standard 11 point option % twoside - standard double-sided pages option % fuzz - Z definitions ("zed" may be used instead) % crest - Oxford University arms (optional) % pounds - non-italic pound sign (optional) % Page usage \oddsidemargin 1pt \evensidemargin 1pt \marginparwidth 30pt \topmargin 1pt \headheight 1pt \headsep 1pt \footskip 24pt \textheight 650pt \textwidth 460pt % Paragraph format \parindent 0em \parskip 1ex % Macro definitions % General definitions \def\Z{{\bf Z}} \def\ie{i.e.\ } \def\eg{e.g.\ } \def\etc{etc.\ } \def\htab{\hspace*{0.375in}} % Z notation \def\Defs{\ ==\ } \def\minischema#1{\begin{minipage}[t]{1.75in}\begin{schema}{#1}} \def\endminischema{\end{schema}\end{minipage}} % Sessions, topics and breaks \def\Session#1#2#3{\section{#2}} \def\Topic#1#2{\subsection{#1 \ \ {\em #2}}} \def\Break#1#2{\subsection*{#2}} \def\heading#1{\subsubsection*{#1}} % Mike Spivey's "official" fuzz macro \def\fuzz{{\large\it f\kern0.1em}{\normalsize\sc uzz}} % Title information \title{Proceedings of the Third Annual \\ \Z\ Users Meeting \\[1.5ex] {\normalsize at the} \\ {\large Department of External Studies} \\[-0.75ex] {\large Rewley House, 1 Wellington Square, Oxford} \\ {\normalsize on} \\ {\large Friday, 16th December 1988}} \author{compiled, edited and written by \\ Jonathan Bowen} \date{} % Start of document \begin{document} \begin{titlepage} \maketitle \thispagestyle{empty} \vspace{1.0in} \begin{center} {\em Programme Committee} \\[0.5ex] Jonathan Bowen \\ John Nicholls \\ Jim Woodcock \vspace{0.5in} \crest \\[2ex] Oxford University Computing Laboratory \\ Programming Research Group \\ 8--11 Keble Road \\ Oxford\ \ OX1 3QD \end{center} \newpage \thispagestyle{empty} Further copies of this Proceedings, PRG monographs and other \Z\ related material are available. For more information, please contact: \begin{tabbing} Xxxxx: \= 0000-000000\ \ \= \kill \> The Librarian \\ \> Oxford University Computing Laboratory \\ \> Programming Research Group \\ \> 8--11 Keble Road \\ \> Oxford\ \ OX1 3QD \\ \> England \\ \ \\ Tel: \> 0865-273837 \> (general enquiries) \\ \> 0865-273838 \> (librarian) \\ Fax: \> 0865-273839 \\ Email: \> {\tt library@uk.ac.oxford.prg}\ \ (JANET) \end{tabbing} \end{titlepage} \thispagestyle{empty} \tableofcontents \newpage \setcounter{page}{1} \Session{9.30}{Introduction}{John Nicholls, PRG} On 16th December 1988, the third annual \Z\ Users Meeting was held at 1 Wellington Square, Oxford. John Nicholls, a Research Officer in the Programming Research Group (PRG) at Oxford University, chaired the meeting, as last year. Over 90 delegates from industry, academia and other research establishments were present representing a good cross-section of those who use and are interested in \Z. \Topic{Chairman's address}{John Nicholls, PRG} John Nicholls welcomed delegates to this, the third \Z\ Users Meeting. There were several new aspects of this meeting, including the organisation of {\em two} Tutorials (one on refinement, the other on proof) and a Workshop on ``\Z\ in the development process''. Feedback from attendees at these events indicated that they had been successful. One purpose of the \Z\ Users Meetings is to exchange information on progress and achievements by members of the \Z\ community. This year, we are pleased to welcome a number of new users, and also to see that established users have made significant advances. The meetings also provide an opportunity for attendees to express opinions or concerns about the direction of \Z. In previous meetings, concerns have been expressed about the need to stabilise and standardise the notation, the inclusion of facilities for concurrency and refinement, and the provision of \Z\ tools. In the past year, progress has been made on all of these topics, and a particularly noteworthy event has been the completion and publication of the {\em \Z\ Reference Manual}, an important step towards the standardisation of \Z. At the time of the meeting, discussions were being held about an IED project for \Z\ standards and \Z\ tools, and a brief review of this project is made in the meeting. Coming fresh from attending the workshop at which the software development process was being discussed, (the speaker John Nicholls) was tempted to consider the process by which a notation and method such as \Z\ is developed. We can distinguish the following stages: \begin{enumerate} \item ``It exists.'' The objectives and philosophy are established. \item ``It is thus.'' There is then a period of stabilisation and consolidation. \item ``It is used like this.'' \item ``And it has this value.'' Finally there is an assessment phase. \end{enumerate} \Z\ has firmly passed the first stage, is well into the second stage, but has only started to enter the last two stages. \Topic{Keynote speech}{Martyn Thomas, Praxis Systems plc} Martyn Thomas, the Chairman of Praxis Systems plc, was invited to give the keynote speech for the day. He started by thanking the audience for being at the meeting and apologising for having to leave immediately after his speech to attend another prior engagement. His talk was entitled \begin{quote} {\large ``The future of Formal Methods''} \end{quote} \heading{Professionalism} He presented the audience with a quotation: \begin{quotation} `` \ldots these formal methods are the key to writing much better software. Their widespread use will revolutionise software writing, and the economic benefits will be considerable -- on a par with those of the revolution in civil engineering during the last century.'' \end{quotation} \begin{flushright} Brian Oakley\\ ``Alvey Achievements''\\ June 1987 \end{flushright} In the future we must be more precise. Only four years ago people involved with formal methods were regarded as ``loonies''. Now things are different; people apologise for {\em not} being formal at conferences. In the UK and Europe we have a world competitive edge in the area of formal methods. \heading{Formal Methods are not a panacea} \begin{itemize} \item We shall never be able to achieve certainty. There are good philosophical reasons for this. \item We cannot quantify the probability of error. There is no sign that we shall be able to do this before the end of the century. \item We must convince others by demonstration, not argument. The cost benefit must be shown. \newline We need publishable evidence of improvements in quality and productivity. Please write up and publish such evidence -- or send it to Martyn Thomas who will do this for you! \end{itemize} \heading{We need a technical intrastructure} \begin{itemize} \item Tools -- which should themselves be verified. These may be simple (type-checkers, cross reference generators, etc.) or complex (e.g.\ support for rigorous development). Why use formal methods for development and then use an unverified optimising compiler? We also need verified compilers. \item Standards -- defining levels of use of formal methods, to be used in procurement. \item The infrastructure is important -- we need a programme of developing key, verified tools and adopting them. If we don't act as if we feel formal methods are important, why should anyone else? We must use formal methods ourselves and formal verify software which we generate if we are to convince others of the benefit of the approach. \item We must maintain balance. Using formal methods without a QMS\footnote{Quality Management Standard.} is unbalanced. Using formal methods without conventional methods is unbalanced. \end{itemize} \heading{Safety -- a major issue} Safety-related computer systems are a major policy issue. Formal methods are important for safety -- this is a useful pressure point on industry. If we cannot win the argument here, then we cannot win anywhere, particularly in the short term. The current state of play is lamentable; formal methods are almost unused for safety-critical systems apart from the CEGB\footnote{Central Electricity Generating Board.} and for military applications.\footnote{Rolls Royce are also using formal methods for safety critical systems.} Project managers are conservative -- using unproven technology is avoided for good reasons. Even if formal methods were just used for specification then the rate of production of safety critical systems would be reduced drastically. In addition, formal methods are not politically acceptable yet. We need: \begin{itemize} \item A definition of the acceptable minimum development practices; \item A definition of realistic best practice; \item Mandatory registration of safety-related systems and mandatory incident-reporting. \end{itemize} What can we realistically expect? Formal methods should be mandatory. \heading{A long-term goal} We should aim to have formal methods in widespread use. We need a Trojan horse, for example, a formal SSADM, to bring semantic checking to a wider user base. There should be more information in the specification and more rule checking. In the 1970s, strong typing and high level languages made right-first-time programming a realistic goal for many programmers. I would like us to provide the methods and tools for right-first-time specification and design, for the wider community, in the 1990s. \heading{Questions} Q: There is a boot-strapping problem with verification. How many times do you need to do this to be sure? (For self-compiling compilers you can check for stabilisation of the binary code.) A: This is a philosophical problem -- but possibly not a practical problem. Q: For RISC\footnote{Reduced Instruction Set Computer.} machines, the verification problem has been moved from the hardware to the compilers. On USENET there has recently been a study of optimising compilers, all of which where found to be breakable. Any comments? A: Many compilers are very complicated and bound to be bug-ridden. Programming in full Ada is an enormous act of faith which would stagger most monks! C is full of problems. However even assuming the compiler is correct, we still depend on the hardware. This is not necessarily reliable; for example, most PCs do not have memory parity checking. \Session{10.15}{\Z\ standards, tools and education}{} \Topic{\Z\ standards}{Rosalind Barden, Logica} Rosalind Barden of the Advanced Software Engineering Group at Logica Cambridge Ltd gave this presentation instead of Tim Hoverd as previously advertised. The brief of this group is broadly to investigate and research areas which may be useful in 2--5 years' time. Rosalind described an IED\footnote{Information Engineering Directorate -- a successor to Alvey.} project proposal with the objective to produce a \Z\ standard. This would use Mike Spivey's ``The \Z\ Notation: A Reference Manual'' as a starting point. \heading{ZEM -- towards a method for the application of the \Z\ notation} (or \Z\ and the art of motorcycle maintenance!) \heading{Overview} The partners are: \begin{itemize} \item Logica Cambridge Ltd \item IBM \item Programming Research Group \end{itemize} The proposal is for three year project at a total cost of \pounds710,000. \heading{Work Programme} It is felt that now is the time to strike for the standardisation of \Z. The project aims to produce an evolving \Z\ standard with regular reviews. It will use Mike Spivey's ``The \Z\ Notation: A Reference Manual'' as input. A goal is to assist and extend the industrial use of \Z. The project would also be involved in the development of \Z. It will undertake case studies in concurrency and the (formal) definition of concurrency extensions to \Z. It will also investigate case studies in refinement and produce a refinement notation. A methods hand-book will be written. This will be based on: \begin{itemize} \item A survey of experienced \Z\ users, \item Case studies of ways of using \Z. \end{itemize} \heading{Dissemination} The work will be in the public domain. There will be regular reviews of documents and a number of workshops will be held. Volunteers will be required for \begin{itemize} \item The standards review body \item Case studies \item User survey \end{itemize} Please form an orderly queue! In the question and answer session the following points were raised. \begin{itemize} \item It should be noted that this is only a {\em proposal} at the moment. It has passed the first stage and a full proposal has been submitted to the IED. \item This project might delay standardisation (being a three year project). \item There was a question as to what will happen if this project is not approved -- will it happen anyway? \end{itemize} \Topic{Tool requirements}{Mike McMorran, IBM} Mike McMorran of IBM, Winchester gave a talk on \Z\ tools for the PS/2 personal computer. This work is in conjunction with Polytechnics. Around 20 people were surveyed to discover the user requirements for such tools. One requirement was to ``stop changing the system'' since minor changes in symbols causes problems with tools. \heading{PS/2 tools} The basic PS/2 tools include: \begin{itemize} \item A live parsing editor ``LPEX''. This is a syntax driven editor which can handle C, REX, GML, etc. A parser for the GML mark up language with \Z\ extensions was developed. In the future this may be extended to support the use of SGML. An investigation of the human factors involved in the entry of \Z\ into a computer is seen as important. Entry aids to help with \Z\ symbols and schema boxes are beneficial. \item Printing facilities. A number of special printer fonts are needed. \item Schema inclusion. This is a simple pragmatic tool for textual rather than mathematic manipulation. Area of interest include: \begin{itemize} \item Schema windows. \item Schema calculator. (Expanding schemas.) \item Expression simplifier. \item Consistency checker. (Avoiding $false$ in predicates.) \end{itemize} \end{itemize} \heading{Desirable tools} There are other areas which could benefit from mechanical tools. Some examples follow. Aid with schema factoring is desirable. For example, given two schemas $A$ and $B$, which parts can be factored out into a third schema $C$? \begin{center} \vspace*{-2ex} \begin{minischema}{A} \ \where\ % \end{minischema} \htab \begin{minischema}{B} \ \where\ % \end{minischema} \\ \begin{minischema}{C} \ \where\ % \end{minischema} \htab \begin{minischema}{A} C\\ \vdots\where\ % \end{minischema} \htab \begin{minischema}{B} C\\ \vdots\where\ % \end{minischema} \end{center} Checking for schema completeness is useful. For example in \begin{zed} Add \defs AddOK \lor AddDep \lor AddError \end{zed} are all situations covered by the three component schemas? The calculation of pre- and post-conditions for an operation schema is useful. For example, the pre-condition may be calculated by hiding (existentially quantifying) all the output and {\em after} state components. Help with proofs concerning pre- and post-operation predicates would be useful. E.g.: \begin{center} \vspace*{-2ex} \begin{minischema}{State} x:\nat\where x\leq 255 \end{minischema} \htab \begin{minischema}{Op} \Delta State\\ \vdots\where x'=x+1 \end{minischema} \end{center} Here of course $x'\leq 255$, so $x\leq 254$ is a pre-condition for $Op$ to succeed. Such restrictions may not be so obvious in more complicated cases. \heading{Design tools} A number of useful tools to aid the software design process have been identified: \begin{itemize} \item Refinement assistant, including refinement verification. \item Code sanity checker to identify code which {\em could} be a refinement and code which {\em cannot} be a refinement. \item Multi-parser, which will check the \Z\ specification, the design notation and the code. \end{itemize} For successful design using formal methods, the whole project must be committed to their use. They are not effective on an individual basis. \heading{Other tools} A number of other tools and facilities which could be helpful have been suggested: \begin{itemize} \item A tool to check for house style. \item A schema library. \item An informal text linker to relate the corresponding informal text with the formal text. \item A schema structure diagram generator. \item Measurement support. \item On-line reference manual (for example, Mike Spivey's ``The \Z\ Notation: A Reference Manual''). \item Context sensitive help. \end{itemize} \Topic{COMETT \Z\ course}{Jonathan Bowen, PRG} Jonathan Bowen of the Programming Research Group described work currently being undertaken at the PRG on the distribution of material for a ``COMETT''\footnote{Although this has been nicknamed the ``COMETT'' course, I understand the funding is actually being provided by the UGC (University Grants Committee).} \Z\ course in the not-too-distant future. This is based on the existing \Z\ course at Oxford, given at least every summer at an Oxford college, and also as demand dictates. It will include comprehensive printed material (using the document preparation system \LaTeX\footnote{This document has been prepared using the same text formatting system.}\ for which \Z\ macros exist). The material will be designed for use by teachers of \Z\ rather than end users. The idea is that teachers in industry and educational establishments should be able to obtain the material and use it as a basis for their own courses on \Z. \heading{Material} The material provided will consist of: \begin{itemize} \item Lecture notes -- these are designed to be given to students on the course and covers what the teacher says during the lectures. \item Overhead projector foils -- these will be based on the lecture notes. \item Teacher's notes -- these include motivation for the lectures covered, points to be covered when presenting the foils and quick-fire questions which may be used to check that the students are following the material. \item Exercises and solutions. \end{itemize} \heading{Sessions} The course consists of a number of $1\frac{1}{2}$ hour sessions (four per day is recommended). A typical breakdown would be: \begin{center} \begin{tabular}{lc} {\bf Topic} & {\bf Sessions} \\[0.5ex] Motivation & 1 \\ Mathematics & 4 \\ Proofs & 1 \\ Structuring and use & 5 \\ Case studies & 3 \\ Exercises & 3 \\ Workshop & 10 \end{tabular} \end{center} The workshop is optional, but it has been found to be very valuable in practice. The course participants are divided into teams of approximately 3--4 people and given a problem to specify in \Z. Some refinement of the specification towards code may also be undertaken if desired, as time permits. In any case, it is recommended that anyone attending a \Z\ course should attempt some sort of \Z\ specification as soon as possible after the course to allow the ideas to be tried out in practice. Material for each session is being prepared by members of the PRG and is reviewed by an least one other member of the PRG. The material has also been tested on the 1988 summer \Z\ course at Oxford. All being well, the material will be made available sometime in 1989. Arrangements on how the material is to be distributed have not yet been finalised. It is intended that the material should be made available to anyone who wants it. The charge (as yet undecided) will be designed to cover costs rather than make a huge profit. Details of the course will be sent to all \Z\ Users Meeting participants as soon as it is available -- if possible, please refrain from enquiries until this time! \Break{11.00}{Coffee break} \Session{11.20}{Technical presentations}{} \Topic{A Miscellany of Handy Techniques}{Ruaridh Macdonald, RSRE} Ruaridh Macdonald of RSRE,\footnote{Royal Signals and Radar Establishment} Malvern, presented a number of techniques in \Z\ which have been used at RSRE in the formal specification of part of a compiler. A paper covering the subject of his talk is included with these Proceedings. \Topic{Free Type Definitions}{Mike Spivey, PRG} The \Z\ construct for ``free type definitions'' (sometimes called ``data type definitions'') provides a powerful way of describing recursive types. For example, here is a free type definition describing binary trees of numbers: %%unchecked \begin{zed} TREE ::= empty | fork \ldata \nat \cross TREE \cross TREE \rdata. \end{zed} The meaning of this definition can be explained by translating it into other \Z\ constructs. We first introduce a new basic type $TREE$, the set of binary trees: \begin{zed} [TREE]. \end{zed} The empty tree is a constant of type $TREE$, and $fork$ is a function taking a number and two trees and giving another tree: \begin{axdef} empty: TREE \\ fork: \nat \cross TREE \cross TREE \inj TREE \end{axdef} We use the injection arrow $\inj$ to reflect the fact that $fork$ makes different trees from different components. Two axioms add more information about the type $TREE$. The first, a {\em disjointness\/} axiom, says that $empty$ is not one of the trees that can be constructed with $fork$: \begin{zed} empty \notin \ran fork. \end{zed} The second axiom is an {\em induction\/} principle: \begin{zed} \forall S: \power TREE @ \\ \t1 empty \in S \land \\ \t1 fork \limg \nat \cross S \cross S \rimg \subseteq S \\ \t1 \implies TREE \subseteq S. \end{zed} This axiom is the foundation for proof by structural induction on trees. To prove $\forall t: TREE @ P(t)$, we just need to show \begin{enumerate} \item\label{1} $P(empty)$, and \item\label{2} if $P(t_1)$ and $P(t_2)$, then $P(fork(n, t_1, t_2))$. \end{enumerate} To see the validity of this proof method, consider the set \[ S = \{~t: TREE | P(t)~\}. \] Because of (\ref{1}), $empty$ is in S; and because of (\ref{2}), if $t_1$ and $t_2$ are members of $S$ and $n$ is any natural number, then $fork(n, t_1, t_2)$ is in $S$: in symbols, \[ fork \limg \nat \cross S \cross S \rimg \subseteq S. \] The induction axiom allows us to deduce that $TREE \subseteq S$, i.e.\ that \[ \forall t: TREE @ P(t). \] Non-recursive free type definitions are often used to describe error codes: %%unchecked \begin{zed} RESULT ::= ok | none\_left, \end{zed} or to give the effect of ``variant records'': %%unchecked \begin{zed} VEHICLE ::= car \ldata COLOUR \rdata | bike \ldata WEIGHT \rdata. \end{zed} In these cases, the two axioms about the type can be merged into one {\em partitioning\/} axiom. For $RESULT$: \begin{zed} [RESULT] \end{zed} \begin{axdef} ok, none\_left: RESULT \where \langle \{ok\}, \{none\_left\} \rangle \partition RESULT \end{axdef} For $VEHICLE$: \begin{zed} [VEHICLE] \end{zed} \begin{axdef} car: COLOUR \inj VEHICLE \\ bike: WEIGHT \inj VEHICLE \where \langle \ran car, \ran bike \rangle \partition VEHICLE \end{axdef} \heading{The problem of consistency} A free type ``definition'' is no more than a {\em description\/} of a recursive type: there is no reason {\em a priori\/} to suppose that any recursive type exists which satisfies the description. To see that this is a potential source of inconsistency in specifications, consider the following description of the type of ``objects'': \begin{zed} OBJECT ::= file \ldata FILE \rdata | set \ldata \power OBJECT \rdata. \end{zed} An object is either a simple file, or it is a packaged set of other objects. Part of the meaning of this description is that $set$ is an injection from $\power OBJECT$ to $OBJECT$: \[ set: \power OBJECT \inj OBJECT. \] But in fact, no such injection can exist! We can show this by assuming that an injection $set$ exists and deriving a contradiction, namely a variant of Cantor's paradox in set theory. Define a set $C$ of objects by \[ C == \{~V: \power OBJECT | set~V \notin V @ set~V~\}. \] For any set of objects $V$, we can ask whether the object $set~V$ is a member of $V$ itself. The set $C$ contains those objects $set~V$ for which the answer is ``no''. For any set $S: \power OBJECT$, \begin{argue} set~S \in C \\ \t1 \iff (\exists V: \power OBJECT | set~V \notin V @ set~S = set~V) & def.\ of $C$ \\ \t1 \iff (\exists V: \power OBJECT | set~V \notin V @ S = V) & $set$ is an injection \\ \t1 \iff set~S \notin S & one-point rule \end{argue} So $set~S \in C \iff set~S \notin S$. Now substitute $C$ for $S$: we obtain \[ set~C \in C \iff set~C \notin C, \] a contradiction. This contradiction does not mean that the \Z\ construct for free type definitions is unsound; it simply highlights the responsibility of a specification author to check that any free type definitions he or she uses make sense, and underlines the need for general theorems which guarantee consistency. \heading{Finitary constructions} In general, a free type definition looks like this: %%unchecked \begin{syntax} T & ::= & c_1 | c_2 | \ldots | c_m \\ & | & d_1 \ldata E_1[T] \rdata \\ & | & d_2 \ldata E_2[T] \rdata \\ & | & \ldots \\ & | & d_n \ldata E_n[T] \rdata \end{syntax} Here $c_1$, $c_2$, \dots,~$c_m$ are the constants of the type $T$, and $d_1$, $d_2$, \dots,~$d_n$ are the constructors. The domains of the constructors are given by arbitrary set-valued expressions $E_1[T]$, $E_2[T]$, \dots,~$E_n[T]$ which may involve the type $T$ being defined. The consistency theorem guarantees that the recursive type described by this definition really exists by placing restrictions on the constructions $E_i[T]$ which may be used. In its simplest form, the theorem demands that all these constructions be {\em finitary}. A finitary construction $E$ is one for which the result $E[S]$ of applying it to a set $S$ is the same as the union of the sets $E[V]$ obtained by applying it to all {\em finite\/} subsets $V$ of $S$. In symbols, \[ E[S] = \bigcup \{~V: \finset S @ E[V]~\}. \] Broadly speaking, any construction of objects made from only a finite number of elements of $T$ is finitary: for example, \begin{itemize} \item elements $T$, \item pairs $T \cross T$, \item finite sequences $\seq T$, \item finite sets $\finset T$. \end{itemize} Moreover, any composition of finitary constructions is also finitary. But $\power T$ is not finitary, because it includes infinite subsets of $T$ as well as finite ones. Here is the statement of the consistency theorem: \paragraph{Theorem} Any free type definition containing only finitary constructions has at least one model. \heading{Summary} \begin{enumerate} \item Free type definitions are an abbreviation for axiomatic descriptions of recursive types. \item There is a need to prove that free type definitions are consistent. \item By restricting ourselves to finitary constructions, we can be sure of consistency. \end{enumerate} \Topic{Brief introductions to demonstrations}{} During the lunch break a number of tools were demonstrated at the Programming Research Group in Keble Road. \Break{12.45}{Lunch} \Session{13.30}{Demonstrations}{(8--11 Keble Road)} \Topic{Fuzz}{Mike Spivey, PRG} \fuzz\ takes \Z\ in the form of ASCII input which can also be processed by the \LaTeX\ document preparation system to produce a formatted document suitable for output to a laser printer. The tool checks the conformance of the \Z\ in the document by type-checking the contents. By default it uses the standard \Z\ library as detailed in Mike's ``The \Z\ Notation: A Reference Manual''. A listing showing schemas and types can be generated. Currently the tool runs on Sun~3 equipment under Unix and IBM PC compatible machines under MS-DOS. Other machines could be supported -- the tool is written in C with portability in mind. The tool is available on a commercial basis. For more information, contact Computing Science Consultancy, 2 Willow Close, Garsington, Oxford OX9~9AN. \Topic{FORSITE}{Andy Ricketts, Racal} This tool was jointly developed on the Alvey-funded FORSITE project by four sites\footnote{Pun intended I'm afraid!} including Racal and the PRG. It is front-ended by the QED editor and includes facilities for the following: \begin{itemize} \item WYSIWYG\footnote{What You See Is What You Get.} editing of \Z\ documents. \item Parsing of \Z\ documents. \item Type-checking of \Z\ documents. \item Indexing of the schema and component names. \item Individual schema expansion. \end{itemize} The tool is written in C and the functional programming language ML. It runs under Unix on Sun~3 equipment under the SunView window system. The FORSITE project is due to end at the end of March 1989. For more information on the availability of the FORSITE tool, contact Andy Ricketts, Racal Research Ltd., Worton Drive, Worton Grange Industrial Estate, Reading, BERKS RG2 0SB (Tel: 0734-868601). \Topic{Zebra}{Bernard Sufrin, PRG} This is another more recent \Z\ type-checker. It is written in ML. It is less easy to port than Mike Spivey's tool and currently runs on Sun~3 equipment. It is normally interfaced to the WYSIWYG editor QED but could easily be adapted for other formats using conversion tables -- internally the tool uses an ASCII form of the \Z\ document. If anyone is intested in using this software, they should contact Bernard at the PRG -- it is ``more or less public domain''. \Topic{B tool}{Ib S\o rensen, BP} This proof assistant is being developed by Jean-Raymond Abrial in Paris in conjunction with the PRG. It is in use at the PRG and BP. The notation supported is similar to \Z\ but does include all the features of \Z; in particular, schemas are not supported. This is a research tool and is still under development. \Session{14.15}{Project presentations}{(Chairman: Bernard Sufrin, PRG)} \Topic{The use of \Z\ in Tektronix}{Kathleen Milsted, PRG} Kathleen Milsted, currently a D.Phil.\ student at the PRG, spent July to October of 1988 working for Tektronix, Inc., Beaverton, Oregon, U.S.A. \heading{TEKTRONIX, Inc.} Tektronix design, manufacture and sell high frequency oscilloscopes, computer peripherals, and other electronic equipment all around the world. The Computer Research Laboratory have the following interests: \begin{itemize} \item Specification Environments \item Advanced Languages \item Knowledge Based Systems \item Visual Systems \item Application Languages: C, Smalltalk-80, C++, Scheme \end{itemize} \heading{Oscilloscope Design Project} Around half the people in the Tektronix Laboratory are involved in writing software, mainly in C. About a year ago they decided to try using \Z\ (because of personal contact with the PRG) in the Specification Environments Group on an oscilloscope design project (one of their main products). Nowadays oscilloscopes contain more and more software and also multiprocessors. The engineers were asked, ``What is a waveform?'' Their answer was often of the form ``a 1K array of 8-bit digitised samples'' -- a rather implementation-oriented view! The following block diagram gives an overview of an oscilloscope: \setlength{\unitlength}{0.75in} \begin{center} \begin{picture}(6,3.25) \put(0,2.62){Signal} \put(0,2.5){\vector(1,0){1}} \put(1,2){\framebox(1,1){}} \put(2.1,2.62){\shortstack{Wave\\form}} \put(2,2.5){\vector(1,0){1}} \put(3,2){\framebox(1,1){}} \put(4.1,2.62){Trace} \put(4,2.5){\vector(1,0){1}} \put(5,2){\framebox(1,1){}} \put(0.5,2.5){\line(0,-1){1.5}} \put(0.5,1){\line(1,0){1}} \put(1.5,1){\vector(0,1){1}} \put(1.6,1.5){Trigger} \end{picture} \end{center} \vspace{-0.75in} A signal can be considered as a (total) function of time (say nano-seconds) to voltage (say milli-Volts). A waveform can be thought of as some part of this -- \ie a partial function: \begin{syntax} Time & \Defs & \nat \\ Volts & \Defs & \num \\ & & \\ Signal & \Defs & Time \fun Volts \\ Waveform & \Defs & Time \pfun Volts \end{syntax} A waveform can be captured as a trace: \begin{syntax} Horiz & \Defs & \nat \\ Vert & \Defs & \num \\ & & \\ Trace & \Defs & Horiz \pfun Vert \end{syntax} A trace can be triggered by user-specified events. There are a number of channel and trigger parameters to specify the desired configuration: \begin{zed} [ChanPrmtrs, \ TrigPrmtrs, \ Trigger] \end{zed} \begin{axdef} TrigConfig: TrigPrmtrs \fun Signal \fun Trigger \\ \t3 \\ ChanConfig: ChanPrmtrs \fun Trigger \fun Signal \fun Trace \end{axdef} An oscilloscope receives a signal. The channel and trigger parameters control the traces which are captured by the oscilloscope from the signal: \begin{schema}{Oscilloscope} s: Signal \\ cp: ChanPrmtrs \\ tp: TrigPrmtrs \\ ts: \seq Trace \where \forall t: \ran ts \spot \\ \t1 \exists trig: TrigConfig~tp~s \spot \\ \t2 t = ChanConfig~cp~trig~s \end{schema} This modelling helps engineers to understand what an oscilloscope is in a more abstract way than they are used to. \heading{ZEE -- \Z\ Engineering Environment} A support environment for the development of \Z\ specifications called ZEE\footnote{The name ``ZEE'' is an American answer to the insistence of pronouncing the name \Z\ as ``zed''!} is being developed. This has the following features: \begin{itemize} \item Implemented in Smalltalk, \item WYSIWYG editor, \item Parser, \item Type-checker, \item Hypertext capabilities, \item Proof environment (in design): \begin{itemize} \item Simple schema manipulator, \item Emphasis on support for user. \end{itemize} \end{itemize} \heading{Reusable Component Catalogue} Work is also being undertaken on a reusable component catalogue based on a Smalltalk library. For more information, see: {\em Specifying reusable components using Z: Realistic Sets and Dictionaries}, by Ralph London and Kathleen Milsted. Specification styles for object-oriented applications are being investigated. Concerns include object--message orientation and single/multiple inheritance. \smallskip Overall, the management at Tektronix seem to be impressed by \Z, so hopefully this experiment will be continued. \Topic{Working with CORE and \Z: an evaluation} {Brian Hepworth, British Aerospace} Brian Hepworth of British Aerospace gave a talk at last year's \Z\ Users Meeting. He summarised the progress in the use of \Z\ at British Aerospace since then. \heading{Software Technology Department -- Formal Methods Group} The Software Technology Department consists of a number of specialist areas, undertaking research and development over a range of System and Software Engineering topics covering development of life-cycle tools and techniques through to performance evaluations of new hardware architecture, languages and concepts. The Formal Methods Group undertakes research into methods for improving the specification and implementation of real-time software. Recent research has been targeted in the following areas: \begin{description} \item[Use of \Z\ within CORE:] CORE is a semi-formal requirements capture method and statement notation that is used extensively within British Aerospace on very large scale projects. Research into the use of \Z\ applied at various levels within CORE has provided the basis for which formality will be introduced to BAe's current development process. \item[Project application of \Z\ within CORE:] Currently the Formal Methods Group is managing and providing technical support to a project representative pilot study using \Z\ within CORE, in parallel with an on-line project. The objective of this study is to establish the benefits of applying formal techniques to the development process against those applied to the on-line and more conventional development process. \item[Prototyping Specifications:] Many process-control applications specified in \Z\ can be prototyped easily using functional programming languages. As an experiment, the language ``Refine'' has been used to produce prototypes of simple systems. \item[Tools:] British Aerospace have developed the ZED editor which allows \Z\ specifications to be created, modified and printed. Each user has access to the library of specifications which belong to the current project. Mathematical symbols are entered via keywords but displayed as symbols on the terminal. \end{description} \heading{Formal Methods Group Work} The research work concentrates on the following areas: \begin{description} \item[Utility Systems:] Engines, Hydraulics, Fuel, etc. Case studies include: \begin{itemize} \item Hydraulics Control Systems \item Cabin Temperature Control Systems \item Engine Start, Restart, Shutdown Control Systems \end{itemize} \item[Avionic Systems:] Instrumentation, Navigation, Radar, Communications, etc. Case studies include: \begin{itemize} \item Display Management Systems \item Navigation Database Systems \end{itemize} \item[Flying Control Systems] \end{description} A project on ground based test equipment (the AIDASS Hardware Diagnostics System) is also being undertaken to establish the benefits of using \Z. \heading{Case Studies} The initial aim in applying formal methods is to give a more definitive approach to writing process descriptions within CORE. Here is a simple example of a system described using \Z: \setlength{\unitlength}{1.8pt} \begin{center} \begin{picture}(170,70) \put(15,65){\makebox(0,0){$a$}} \put(15,55){\makebox(0,0){$b$}} \put(10,60){\vector(1,0){32}} \put(10,50){\vector(1,0){32}} \put(42,50){\line(1,0){3}} \put(42,60){\line(1,0){3}} \put(45,45){\framebox(30,20){}} \put(75,55){\line(1,0){3}} \put(80,55){\makebox(0,0){$0$}} \put(82,55){\line(1,0){33}} \put(90,60){\makebox(0,0){$control$}} \put(115,55){\line(0,-1){15}} \put(105,45){\makebox(0,0){$true$}} \put(75,35){\vector(1,0){32}} \put(107,35){\line(1,0){3}} \put(110,30){\framebox(30,10){}} \put(112,35){\makebox(0,0){$0$}} \put(125,35){\makebox(0,0){$X$}} \put(140,35){\vector(1,0){32}} \put(155,35){\line(0,-1){20}} \put(165,40){\makebox(0,0){$out$}} \put(115,30){\line(0,-1){10}} \put(90,40){\makebox(0,0){$in1$}} \put(105,25){\makebox(0,0){$else$}} \put(75,15){\vector(1,0){32}} \put(90,20){\makebox(0,0){$in2$}} \put(107,15){\line(1,0){3}} \put(110,10){\framebox(30,10){}} \put(112,15){\makebox(0,0){$0$}} \put(125,15){\makebox(0,0){$Y$}} \put(140,15){\line(1,0){15}} \put(60,55){\makebox(0,0){$W$}} \end{picture} \end{center} \begin{schema}{W} a? : GO\_STATE\\ b? : BOOLEAN\\ control! : BOOLEAN \where a? = go \land b? = true \also control! = true \end{schema} \begin{schema}{X} in1? : \nat\\ control? : BOOLEAN\\ out! : \nat \where control? = true \also out! = 2 * in1? \end{schema} \begin{schema}{Y} in2? : \nat\\ control? : BOOLEAN\\ out! : \nat \where \lnot (control? = true) \also out! = 2 * in2? \end{schema} Here is another example of a control system taken from one of the case studies at British Aerospace: \begin{center} \begin{picture}(170,190) \put(5,145){\makebox(0,0){Gearbox}} \put(20,140){\framebox(10,10){}} \put(30,145){\line(1,0){10}} \put(45,145){\circle{10}} \put(45,170){\vector(0,-1){20}} \put(45,140){\vector(0,-1){80}} \put(55,60){\makebox(0,0){Flight}} \put(55,55){\makebox(0,0){Control}} \put(55,50){\makebox(0,0){Flow}} \put(45,170){\line(1,0){45}} \put(45,110){\line(1,0){20}} \put(65,112.5){\line(0,-1){5}} \put(75,112.5){\line(0,-1){5}} \put(65,107.5){\line(2,1){10}} \put(65,112.2){\line(2,-1){10}} \put(72,115){\line(0,-1){4}} \put(70,115){\line(1,0){4}} \put(70,115){\line(0,1){10}} \put(70,125){\line(1,0){60}} \put(130,125){\line(0,-1){95}} \put(100,110){\vector(0,-1){20}} \put(100,85){\circle{10}} \put(100,85){\makebox(0,0){P}} \put(100,80){\vector(0,-1){20}} \put(118,87.5){\makebox(0,0){Pressure}} \put(118,82.5){\makebox(0,0){Sensor}} \put(115,65){\makebox(0,0){Utilities}} \put(115,60){\makebox(0,0){Flow}} \put(95,120){\makebox(0,0){Isolation valve}} \put(75,110){\line(1,0){25}} \put(90,160){\framebox(30,20){}} \put(140,170){\vector(-1,0){20}} \put(140,170){\line(0,-1){110}} \put(130,30){\line(-1,0){10}} \put(105,15){\framebox(15,30){}} \put(105,30){\line(-1,0){75}} \put(28,19){\framebox(2,2){}} \put(28,29){\framebox(2,2){}} \put(28,39){\framebox(2,2){}} \put(15,40){\makebox(0,0){close}} \put(15,30){\makebox(0,0){auto}} \put(15,20){\makebox(0,0){open}} \put(112.5,10){\makebox(0,0){Control Processor}} \put(150,55){\makebox(0,0){Combined}} \put(150,50){\makebox(0,0){Return}} \put(105,155){\makebox(0,0){Reservoir}} \put(60,145){\makebox(0,0){Pump}} \put(45,145){\makebox(0,0)[l]{$\sqcup$}} \put(45,145){\makebox(0,0)[r]{$\sqcap\!$}} \end{picture} \end{center} \begin{schema}{Select Closed} valve\_select? : \{ open,\ close,\ auto\}\\ valve\_control! : \{open\_vlv,\ close\_vlv\} \where valve\_select? = close \also valve\_control! = close\_vlv \end{schema} \heading{State \& Abstract Data Representation} CORE has no defined representation of state and abstract data. However ad hoc development of CORE notations use the scheme where state data is input to and output from a process with its type defined informally within a data design note. Such problems are avoided when \Z\ is used. \heading{Future Work} British Aerospace plan to continue investigating the use of formal methods. The following work is planned: \begin{itemize} \item Formal program verification techniques and tools, \item Support for future \Z\ tool developments, \item Refinement directed towards Ada code and subsets of Ada for safety-critical systems. \end{itemize} \Topic{Formal definition of Information Systems}{Ib S\o rensen, BP} Bernard Sufrin introduced Ib S\o rensen as a former and future colleague -- he is currently working at BP on leave from the PRG. \heading{Objectives} Ib is currently interested in the software process and the associated quality concerns. The quality of specifications can be increased through the use of: \begin{enumerate} \item Mathematical based verification techniques, \item Rapid prototyping. \end{enumerate} The programmer's productivity can be increased through the use of: \begin{enumerate} \item Computer assisted design and code verification, \item Reusable specifications, designs and algorithms. \end{enumerate} In particular, the following objectives have been identified: \begin{enumerate} \item A notation and methods to be used in a computer aided formal development process should be developed -- \ie doing \Z\ by computer. \item Systems for the automatic generation of proof obligations are needed. It is useful to check the consistency of the specification, the correctness of the representation and the correctness of the algorithm used. \item Systematic procedures for the semi automatic discharge of proof obligations should be developed. Libraries of mathematical laws and reusable proof-strategies are needed. \item Systematic procedures for the semi automatic generation of designs, and code are required. Help with determining the weakest concrete design, a ``Pascalizer'' and automatic code generation are desirable. \item A practical tool for 1--4 should be developed. \end{enumerate} \heading{Overall Approach} The approach being used is along the following lines: \begin{enumerate} \item A mathematical basis is used -- \eg data refinement rules from the PRG and generalised substitution languages. \item Experimental computer-based assistants are being investigated (if we know how to get the computer to do it -- \eg using the B tool, which is currently playing a central role\footnote{The B tool is currently implemented in c8,000 of (subset) Pascal. BP intend to reimplement it formally using B.}). \item Case Studies are being undertaken. e.g.: \begin{enumerate} \item Development of some simple linear access structures from specification to algorithm (\eg stacks, queues, double-ended queues, etc.), \item Development of medium scale information systems from specification to execution, \item Specification of small real-time control systems. \end{enumerate} Currently dealing with concurrency can be a problem. As an example of the size of the case studies, a specification could consist of 50--100 predicates in total; each (expanded) operation uses around 10--20 predicates. Typically, around 5 operations can be verified in a morning using 10--20 step proofs. This gives you great confidence -- you can go to lunch, feel happy, and not worry about it again. \end{enumerate} In conclusion, the concern is what to do with a (\Z) specification once it has been formulated. For practical development computer assistance is needed; in the real world it is not enough just to use pen and paper. \Break{15.45}{Break} % \Session{16.00}{Project presentations (continued)}{} \Topic{Specifying a component of the SAA interface with \Z} {John Wordsworth, IBM} John Wordsworth of IBM, Hursley Park, Winchester presented the problems encountered in specifying a part of the IBM SAA\footnote{Systems Application Architecture} interface in \Z. In IBM, and SAA in particular, there are many TLA's\footnote{Three Letter Abbreviations} -- in fact there are now so many that sometimes ETLA's\footnote{Extended Three Letter Abbreviations!} are needed! SAA is designed to present a standard interface across different IBM machine architectures -- \eg CPIC.\footnote{Common Programming Interface Communications} A formal specification of this interface (largely in \Z) has been produced. This is layered, so \Z\ was particularly suitable since promoted operations could be used. At the bottom level there are around 30 operations on the ``conversation state''. These can be promoted to programs and then to nodes and new operations can be defined at each level. All this can be done with ``classical'' \Z. However there is a problem with a particular operation called ``$confirm$''. This was solved using a suggestion by Peter Lupton:\footnote{Known as the ``Luptonian'' triad!} \begin{zed} confirm\_atomic \\ [\!] \\ confirm\_front\_end \\ \ \rightarrow\ confirm\_back\_end \end{zed} The pre-condition of $confirm\_atomic$ or $confirm\_front\_end$ must be $true$ for the operation to be performed. If both are $true$, either could be executed non-deterministically. If $confirm\_atomic$ is executed, the operation exhibits atomic behaviour. If $confirm\_front\_end$ is executed then $confirm\_back\_end$ is executed subsequently once its pre-condition becomes $true$. Other operations may interleave between the execution of $confirm\_front\_end$ and $confirm\_back\_end$. \Session{16.30}{Panel on future directions}{} The day finished with a question and answer session by a number of \Z\ experts from the PRG: Carroll Morgan, Mike Spivey, Bernard Sufrin and Jim Woodcock. The panel session ended around 5.15p.m. \section{General} \subsection{Posters} Delegates were invited to display and view posters describing research related to the use of \Z\ on the notice boards at the back of the auditorium. Copies of these are included with these Proceedings for delegates at the meeting. \subsection{Questionnaire} A questionnaire was circulated at the meeting to help in making improvements to future meetings. Delegates were asked to mark boxes for ``usefulness'', ``right level'', ``right mix'', ``organisation'' and ``likelihood of reattendance'' as 5 excellent, 4 good, 3 fair, 2 poor, or 1 bad for events which they attended. 44 completed forms were received. Space was also provided for comments. The marks and comments were very variable. The average marks were all around 4. Things that some people did not like were often counterbalanced by people who did like them, so hopefully overall the balance was right. \section*{Acknowledgements} \addcontentsline{toc}{section}{Acknowledgements} Thank you to all the speakers for making the 1988 \Z\ Users Meeting a worthwhile day for all the participants. In particular, thank you to those who provided foils, notes and even \LaTeX\ source to aid the production of this record -- Mike Spivey's account of his talk is included virtually verbatim. Please accept the author's apologies for any mistakes in the transcription from verbal to written form. John Nicholls and others at the PRG gave valuable comments on the first draft of the Proceedings. A copy has also been circulated on the \Z\ Forum electronic newsletter. A special note of thanks must go to the organising secretary, Joanna Pulley, for making the day run so smoothly. Thank you too for the assistance of Joan Arnold in preparing these notes and mastering \Z\ and diagrams in \LaTeX. Finally, thank you to the audience for making the meeting a success. We look forward to seeing you again next year -- the date of the next \Z\ Users Meeting will be Friday 15th December 1989. \end{document} ************************ END OF Z FORUM 4.3 ************************