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!geraint From: Ruaridh Macdonald (on UK.MOD.RSRE) Newsgroups: zforum Subject: Z Forum Issue 3.1 Message-ID: <20 Date: 20 Jan 88 17:08:19 GMT Date-Received: 20 Jan 88 17:14:31 GMT Lines: 1613 20th January 1988 Z FORUM Volume 3 Issue 1 ----------------- ------- ---------------- Today's Topics -------------- JANET Link Fault Tolerant Systems A Brainteaser Domain and Range of Functions Consistency of Datatype Definitions Z Users' Meeting --------------------------------------------------------------------- The last issue of Volume 2 was number 4. --------------------------------------------------------------------- From: SMAN@RSRE (on UK.MOD.RSRE) Date: Wed, 9 Dec 87 09:30 Subject: JANET link There is a possibility that JNT (Joint Network Team) who run JANET (Joint Academic NETwork) could provide a direct link between the JANET gateway at Rutherford and RSRE thus bypassing the UCL route and also giving RSRE better access to JANET. In order for this to happen, requests for such a link must arise from within the academic community, i.e. from the universities that RSRE communicates with. Could all those readers of the Z Forum who are directly connected to JANET please send a message to IAN SMITH to request a link between RSRE and JANET. His address is: NW@uk.ac.daresbury.dlgm ----------------------------------------------------------------------- From: Andrew Lord X2350 Date: Tue, 12 Jan 88 09:31:26 GMT Subject: Fault Tolerant Systems Is anyone using Z to specify fault tolerant systems? I am interested in hearing from anyone who is using Z in this area as I am thinking of applying Z to such systems and would appreciate comments on any previous experience. Thanks for any help, Andy Lord amlo@uk.ac.warwick (JANET) Department of Computer Science, University of Warwick, Coventry CV4 7AL --------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Tue, 12 Jan 88 08:46 Subject: A Brainteaser Can you suggest a neat way of expressing the function 'condense' on sequences which knocks out consecutive repeat occurrences, so that condense <1,1,4,3,3,3,1,5,5,4,4,4,6> = <1,4,3,1,5,4,6> for example? I am particularly interested in a definition which allows proofs to be readily understandable. The particular theorem I wish to prove is the one concerning 'partial condensations'. Given a sequence S, remove SOME of the repeat occurrences from it to produce a sequence T, a 'partial condensation' of S. Then condense S = condense T. For example, if S is the first sequence above and T = <1,1,4,3,1,5,4,4,6>, then condense S = condense T = <1,4,3,1,5,4,6>. Ruaridh --------------------------------------------------------------------- Date: 11 Jan 88 16:38 +0100 From: weigele@de.dbp.uni-frankfurt.informatik.dbis Subject: Domain and Range of Functions It is often the case in specifications that you want to give a name to the domain or the range of function. Given [Person, Book], suppose we have the schema LIBRARY SB users: pset Person books: pset Book books_on_shelves: pset Book on_loan: Book pfun Person ST dom on_loan dint books_on_shelves = {} dom on_loan duni books_on_shelves = books ran on_loan subs users ESB Now we might like to increase readability by calling dom on_loan "books_on_loan", and by calling ran on_loan "borrowers". This could be done (1) using the WHERE construct of Z or by (2) introducing additional schema components with the appropriate equations. Suppose we take the approach of (1), in a schema SCH2 that imports LIBRARY, would the WHERE abbreviations be known (Also, would the WHERE part of the LIBRARY refer to all previous definitions of its predicate part or just to the last)? --------------------------------------------------------------------- Date: Fri, 15 Jan 88 09:43:29 GMT From: mike@uk.ac.oxford.prg Subject: Consistency of Datatype Definitions CONSISTENCY OF DATA TYPE DEFINITIONS by Mike Spivey [This contribution expands on the explanation of datatypes given in 'The Z Notation - A Reference Manual'. It is for the benefit of those wishing to understand the theory that determines which constructions may safely be used in recursive datatype definitions. RM] The notation for data type definitions is useful, because it allows us to introduce a set closed under some operations without giving an explicit model. Exactly because we do not construct an explicit model, however, there is a danger that a data type definition will not be consistent. For example, the definition D ::= number << N >> | function << D --> D >> is not consistent, because however large the cardinality of D is, D --> D has a larger cardinality, so there can be no injection function: (D --> D) >-> D. This argument is due to Cantor, and is usually known under the name "Cantor's paradox". The data type definition itself is used in the semantics of the lambda-calculus, and the need to make sense of it gave rise to the whole fruitful theory of Scott domains. In Z, we work not with domains but with sets, and there the definition is simply inconsistent. How can we make sure not to write definitions with this problem? There is a simple condition on the 'constructions' on the right-hand side of a data type definition which is sufficient to ensure consistency. It is not a necessary condition, but it seems to cover all the cases we meet in practice. The condition is that all the constructions are _finitary_ in a sense explained below. TECHNICAL NOTE: In Scott domains, we restrict the function space D --> D to functions continuous with respect to a certain partial order on D: the trick there is to construct both D itself and the partial order at the same time. Here we are doing something different, namely restricting ourselves to constructions (like the --> here) which are themselves continuous with respect to inclusion. A typical data type definition looks like this: T ::= c1 | c2 | ... | cm | d1 << C1[T] >> | d2 << C2[T] >> (*) | ... | dn << Cn[T] >> where c1, c2, ..., cm are constants of the type, and d1, d2, ..., dn are constructors. The 'constructions' C1[T], C2[T], ..., Cn[T] are set-valued expressions, possibly containing free occurrences of the name T. I write C[T] to emphasize the fact that they depend on T, and I write C[E] to denote the expression derived from C[T] by replacing all free occurrences of T by the set-valued expression E. I call a construction C[T] _monotonic_ if whenever T sub W, then also C[T] sub C[W] (Here T sub W means T is a subset of W). By a chain on a set X, I mean an infinite sequence of subsets of X with each member a subset of the next: CHAIN[X] == { S: N --> P X | ( forall i: N . S(i) sub S(i+1) ) } The limit of a chain is just the union of all its members: == [X] ====================================== | lim: CHAIN[X] --> P X |--------------- | forall S: CHAIN[X] . | lim S = U { i: N . S(i) } ============================================= I call a construction C[T] _finitary_ if it is monotonic, and for any chain S, the limit of the chain lambda i: N . C[S(i)] is equal to the result of the construction C applied to lim S: forall S: CHAIN[X] . (**) lim (lambda i: N . C[S(i)]) = C[lim S]. This property must hold whatever set is taken as the generic parameter X: it should be proved as a theorem generic in X. The property amounts to the fact that C[T] is continuous with respect to set inclusion. Now I claim that the data type definition (*) is consistent provided that all the constructions C1[T], C2[T], ..., Cn[T] are finitary. This theorem is useful, because almost all of the constructions we use in practice are finitary: in particular, finite sets F X, finite sequences seq X, set constants A not depending on T, Cartesian products X x Y, ... are all finitary, and the composition of two finitary constructions is again finitary. This is all we need to know to check that most definitions are consistent, but if a new construction is introduced, it can be proved finitary by proving a theorem of the form (**) expressed in Z terms. The rest of this article is a proof of the theorem I have just stated: if you are only interested in what rules to follow, you can stop reading here; if you want to be convinced that the rules are right, read on. To prove the theorem, I will construct a model for the data type definition (*), using the fact that the constructions Ck[T] are finitary. To do this, I will have to step outside the typed world of Z for a while and work in ordinary (untyped) set theory. We can begin by simplifying (*) a little. We can eliminate the constants ck by replacing them with constructors ck' acting on the one-point set { 0 }: instead of ... | ck | ... we write ... | ck' << { 0 } >> | ... . When we have built a model for this data type definition, we can define ck to be ck'(0) and derive a model for the original one. Now we can assume the data type definition has the form T ::= d1 << C1[T] >> | d2 << C2[T] >> | ... | dn << Cn[T] >> with all the contructions Ck[T] finitary. We define a chain S of sets by taking S(0) = {} S(i+1) = F[S(i)] where F[X] = { x1: C1[X] . (1, x1) } u { x2: C2[X] . (2, x2) } u ... u { xn: Cn[X] . (n, xn) }. The union operators here are joining together sets which would have different types in Z, so we really need to escape into untyped set theory. At each stage i+1, we perform each construction Ck on S(i), label the results by pairing with k (to ensure disjointness) and gather all these pairs together into S(i+1). Any finitary construction is monotonic, so F[X] is itself monotonic, and S really is an increasing chain of sets. We can prove this by induction: S(0) = {} sub S(1), and if S(i) sub S(i+1) then S(i+1) = F[S(i)] sub F[S(i+1)] = S(i+2). TECHNICAL NOTE. We construct the chain S by recursion. Strong recursion is needed, because S(i+1) is given in terms of S(i) by the 'construction' F[X] which is a 'class-function' or 'ZF-definable operation' and not a set-theoretic function itself. This is another reason for escaping from the Z type system. Now take T = lim S, and for each k define dk: Ck[T] >-> T by dk(x) = (k, x). It's obvious that dk is an injection, and obvious that the ranges of the dk's are disjoint, but is dk(x) always in T? It is, for suppose x in Ck[T]. Because T = lim S and Ck is finitary, we have x in Ck[T] = Ck[lim S] = lim (lambda i: N . Ck[S(i)]). But the limit of (lambda i: N . Ck[S(i)]) is just the union of all the sets Ck[S(i)], so there is an i such that x in Ck[S(i)], and so dk(x) = (k, x) in F[S(i)] = S(i+1) sub lim S = T. So now we have our set T and injections dk: Ck[T] >-> T. It remains to check that the induction principle holds: that if W: P T is such that d1(|C1[W]|) u d2(|C2[W]|) u ... u dn(|Cn[W]|) sub W, (***) then T sub W. The left-hand side of (***) is just F[W]. I shall show by induction on i that S(i) sub W: it follows that T = lim S sub W. For the base case, we see that S(0) = {} sub W. For the step case, suppose S(i) sub W. Then S(i+1) = F[S(i)] sub F[W], since F is monotonic, and because F[W] sub W, we have S(i+1) sub W. This completes the proof. We had to step outside the Z world to perform this construction of a model for the data type definition, but the nice thing, I think, is that the conditions on which it depends, that the constructions Ck are finitary, can be stated and proved inside the world of Z. --------------------------------------------------------------------- Date: Fri, 15 Jan 88 11:13:47 GMT From: bowen@uk.ac.oxford.prg Subject: Z Users' Meeting The Z Users Meeting proceedings is almost finished. It WILL be sent out, but unfortunately one of our secretaries left at Christmas so we are rather short staffed and very busy because it is the start of term. Anyone who URGENTLY needs a copy quickly can contact me. Best wishes for 1988. -- Jonathan [The following is extracted from a LaTeX source file for the benefit of those who will not automatically receive a printed copy. If you want the full LaTeX source with formatting instructions, etc., contact either Jonathan or myself. RM] ------------------------- snip snip ------------------------ % Proceedings of Z Users Meeting, Oxford, 8th December 1987. {\em Programme Committee} \\ John Nicholls \\ Jonathan Bowen \\ Jim Woodcock \\ Oxford University Computing Laboratory \\ Programming Research Group \\ 8-11 Keble Road \\ Oxford OX1 3QD \section{Introduction} On 8th December 1987, the second 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, taking over from Ib S{\o}rensen (a lecturer at the PRG) who organized the meeting last year. 74 delegates from industry, academia and other research establishments were present representing a good cross-section of those who are interested in \Z. % Summary of Z work since last meeting \section{Annual Report} After an initial welcome, John Nicholls presented a summary of the work undertaken on \Z\ at the PRG since the last meeting. The presentation was split up into a number of topics: \nopagebreak \begin{description} \item[Standards.] At last year's meeting, the general consensus was (at least from people outside the PRG!) that \Z\ needed to be standardized to make it more acceptable and useful to industrial users and to enable tools to be produced. This has been attacked on two fronts at the PRG in the last year. A draft document entitled {\em Z: Grammar and Abstract and Concrete Syntaxes} by Steve King et al.\ has been produced, giving a BNF style description of a standard syntax. This was distributed at the meeting, and a final version is due to appear as a PRG monograph shortly. Additionally, Mike Spivey has produced a draft of a {\em Z Reference Manual}, based on Bernard Sufrin's {\em Z Handbook}, of which more later. These documents could be merged. Additionally a less formal {\em Z User Manual} including more examples could be useful. Such a manual has been produced by IBM although the present version is not up to date with the latest \Z\ syntax. Users are invited to express their views on the need for an informal manual. Standards are important for stability. They should be clear and give a mathematical underpinning to the notation. If desirable, a Standards Group could be set up with the help of the PRG. The PRG will concentrate on basic theoretical research as well as joint work with industry to investigate the practical use of formal methods. Additional work is being done to provide guidelines for proof methods using \Z. \item[Tools.] It was suggested that these may be split into basic tools (\eg producing \Z\ documents on a PC) and intermediate/advanced tools (\eg {\em FORSITE} on a Sun workstation). More information is included on both these areas later. \item[Refinement \& Concurrency.] These are vital aspects of a general development method. Linking \Z\ and CSP would be useful to cover concurrency. Talks on these two areas were presented later. \item[Communication.] A number of methods of communication within the \Z\ community were discussed. \begin{description} \item[Z forum.] Ruaridh Macdonald of the Royal Signals and Radar Establishment (RSRE) at Malvern edits an electronic newsletter called {\em Z forum}. This is made up of short articles, requests and so forth contributed by readers. Anyone with an e-mail address on PSS, the academic network JANET, the UUCP network UKnet or many other networks connected to these may receive issues as they are produced and submit entries by contacting Ruaridh on {\tt rm@uk.mod.rsre} or {\tt rm\%uk.mod.rsre@uk.ac.ucl.cs.nss} on JANET. \item[Z bibliography.] A selected bibliography by Jonathan Bowen was distributed at the meeting. This document gives a current list of \Z\ references available either from the librarian at the PRG or as published papers or technical reports from other institutions. A master list which also includes unpublished work has been compiled by the editor of the {\em Z forum}, Ruaridh Macdonald. The list is maintained in electronic form (in {\sc unix} {\em refer} bibliography format). If you have any new references for this list or want a copy of it, please contact Ruaridh, via e-mail if possible at the same address given under {\bf Z forum} above. \item[Posters.] Posters describing research work, etc., were invited from the participants of the meeting. These were displayed at the meeting and are also attached to these Proceedings. \end{description} \end{description} \noindent The idea of a \Z\ Users Group was mooted for discussion (see section under {\bf Future Work} later). \section{Work at the PRG} A number of presentations on work on \Z\ at Oxford were given by members of the Programming Research Group. \subsection{Z Standards: Syntax, Ib S{\o}rensen} A history of the evolution of \Z\ in terms of key work was presented. \begin{tabbing} XX \= 1980/81X \= XXXX \= \kill \> 1979 \> The Specification Language Z (Abrial et al.) \\ \> \> \> (ADA-like) \\ \halfline \> 1980/81 \> The Basic Library (Abrial et al.) \\ \> \> \> (Cliff Jones influence, VDM) \\ \halfline \> 1982 \> A Theoretical Foundation to Formal Programming (Abrial) \\ \> \> \> (Burstall/Scott influence, Set Theory) \\ \halfline \> 1983 \> \Z\ Handbook (Sufrin) \\ \> \> \Z\ Schema Notation (Morgan) \\ \> \> \Z\ Reference Card (Hayes) \\ \> \> \> (Semantics --- DPhil thesis --- Spivey) \\ \halfline \> 1986/87 \> Structuring Specifications --- Schemas (Woodcock) \\ \> \> \Z: Grammar and Concrete and Abstract Syntax (King) \\ \> \> \Z\ Reference Manual (Spivey) \end{tabbing} \noindent Throughout this period, case studies in the use of \Z\ were also being undertaken. The {\em Z: Grammar and Concrete and Abstract Syntax} was requested at last year's \Z\ User Meeting. This work was supported by IBM. The contents include: \nopagebreak \begin{itemize} \item{Grammar in BNF.} \item{Standard terminology.} \item{Appearance and layout.} \item{Scope and type rules (informally).} \item{Abstract Grammar of \Z\ (in \Z).} \end{itemize} \noindent Details of the grammar cover: \nopagebreak \begin{itemize} \item{Document structure.} \item{Language of {\em Definitions}.} \item{Language of {\em Theorems}.} This is not yet stable since no extensive case studies have been undertaken yet. Theorems are currently not included in the {\em Z Reference Manual}. \item{Language of {\em Predicates}.} This has been stable since the early days of Abrial. \item{Language of {\em Terms}.} (Abrial's name --- Mike Spivey uses the name {\em Expressions} in the {\em Z Reference Manual}.) \item{Language of {\em Schemas}.} \end{itemize} \noindent The concrete and abstract syntaxes are not split in this document, although they could be in a course on \Z. Details of terminal symbols (\eg {\tt Z} to start a \Z\ section and {\tt EZ} to end a \Z\ section) are also covered. The target readers for this document include: \nopagebreak \begin{itemize} \item{Tool writers} \item{Educators} \item{Manual writers} \item{Expert users --- not {\em naive} users} \end{itemize} \noindent This has been used as a working document within the PRG. It is due for publication as a PRG monograph early in 1988. \subsection{Z Reference Manual, Mike Spivey} In starting, Mike noted that a \LaTeX\ style file ({\tt zed.sty})\footnote{This document was produced using this style file.} for printing \Z\ specifications is available from him if you can contact him by electronic mail. His address is {\tt mike@uk.ac.oxford.prg} on JANET. Mike then continued his talk with a quotation: \nopagebreak \begin{quote} {\em Jack\/}: You're quite perfect, Miss Fairfax. {\em Gwendolen\/}: Oh! I hope I am not that. It would leave no room for developments, and I intend to develop in many directions. \begin{flushright} Oscar Wilde, {\em The Importance of Being Earnest} \end{flushright} \end{quote} \noindent If possible, a standard should leave room for future developments. The {\em Z Reference Manual} contains a minimal language for \Z\ specifications, a subset of the language described in the {\em Z: Grammar and Concrete and Abstract Syntax} document. For example, theorems and the importing of one document into another are not included. However, this minimal language may be added to, if necessary for a particular specification, but on the same mathematical basis. At present the {\em Z Reference Manual} is in draft form and will be submitted for publication as a book; Mike proposed the following time-scale of events: \nopagebreak \begin{itemize} \item{December 1987.} Draft available for review. \item{1st April, 1988.} End of review period. \item{1st November, 1988.} Proposed date for publication. \end{itemize} A copy will be sent to all participants of the \Z\ User Meeting. People are invited to review the draft and send comments and reactions back to Mike at the PRG. The objective is to make the document understandable and readable, unlike many other standards. It uses examples sometimes, where appropriate. Algebraic laws are also included. Mike then gave a short introduction to the difference between the {\em generic definition} and the {\em axiomatic description} in \Z. A {\em generic definition} may have generic parameters and must make a unique definition: \nopagebreak \begin{gendef}{X} {\rm declaration} \where {\rm predicate} \end{gendef} An {\em axiomatic description} has no generic parameters and may make a loose (\ie a possibly non-unique) definition: \nopagebreak \begin{axdef} {\rm declaration} \where {\rm predicate} \end{axdef} Looseness or liberality may be useful in the the following cases. An informal explanation of which is meant should also be included. \begin{itemize} \item{To give freedom for the implementor.} E.g., the coding of directories as data blocks. \item{To allow details to be fixed later.} E.g., the maximum number of users --- a system option. \item{When the details are irrelevant.} E.g., the coding of characters as nat{\nolinebreak}ural numbers. \end{itemize} The question may arise, ``Why not have loose generic definitions?'' Consider the following example: \nopagebreak \begin{gendef}{X} left, right : X \where left \neq right \end{gendef} \noindent How should the following points be resolved? \nopagebreak \begin{itemize} \item What about $left[\{0\}]$ and $right[\{0\}]$? They are both forced to be $0$, despite the axiom $left \neq right$. \item What about $left[\empty[\nat]]$? It must be a member of $\empty[\nat]$, because of the declaration $left : X$; but $\empty[\nat]$ has no members! \item Is $left[X]$ always the same? \item Is $left[\num]$ the same as $left[\nat]$? \end{itemize} \noindent There is a lot of information which is curiously hidden. Therefore it makes sense to insist that there is exactly one model. \subsection{Z and Concurrency, Jim Woodcock} Jim Woodcock, a Research Fellow at the PRG, presented some work on adding the facilities of CSP to \Z, without changing the current features of \Z. A number of rules for splitting operations in parallel are needed. Jim gave an example of a telephone exchange. First he described the system from a subscriber's point of view. A {\em T}elephone may be either not ringing or ringing: \nopagebreak \begin{tabbing} \htab $T$ \= $\defs$ \= $(lift \THEN S)$ \\ \> $\nondetchoice$ \> $(lift \THEN R)$ \end{tabbing} \noindent where $\nondetchoice$ denotes non-deterministic {\em internal} choice (\ie internal action in the system, outside the control of the subscriber). Once a subscriber has lifted the receiver and {\em S}eized the line, he may then put the telephone down or dial a digit: \nopagebreak \begin{tabbing} \htab $S$ \= $\defs$ \= $(clear \THEN T)$ \\ \> $\detchoice$ \> $(dial \THEN D)$ \end{tabbing} \noindent where $\detchoice$ denotes deterministic {\em external} choice (\ie action by the subscriber). Whilst {\em D}ialing, a subscriber may put the telephone down or dial a digit. The system can detect when enough digits have been dialled: \nopagebreak \begin{tabbing} \htab $D$ \= $\defs$ \= $(clear \THEN T)$ \\ \> $\detchoice$ \> $(dial \THEN D)$ \\ \> $\nondetchoice$ \> $(clear \THEN T)$ \end{tabbing} A {\em R}ecipient can hang up and then lift the receiver to reestablish the call. The other subscriber could hang up or the initiator could hang up. \begin{tabbing} \htab $R$ \= $\defs$ \= $(clear$ \= $\THEN (lift \THEN T))$ \\ \> \> \> $\nondetchoice$ $T)$ \\ \> \> $\nondetchoice$ $S$ \end{tabbing} \noindent (Note that the description above has abstracted away from speech!) An abstract view of the state of the telephone exchange can be provided as a standard \Z\ schema, and operations on this state may be defined in the normal way by relating before and after states. In addition to the standard subscriber operations, there is a demon $Connect$ operation which allows the system to make connections between subscribers. Theorems about the state and the operations are easier to prove because there is a global state in the abstract description. \begin{center} \begin{picture}(200,160) % The telephone exchange % First a schema in thin lines (default) \thinlines \put( 70,100){\line(1,0){60}} \put( 70, 80){\line(1,0){30}} \put( 70, 60){\line(1,0){60}} \put( 70, 60){\line(0,1){40}} % Outline of exchange in thick lines \thicklines \put(100, 80){\oval(80,60)} % Phones and connections \put(0,0){\usebox{\threephones}} \end{picture} \end{center} \noindent However in practice the exchange will be implemented as a number of distributed interconnected subsystems with a relay for each subscriber. \begin{center} \begin{picture}(200,160) % Telephone exchange \thicklines \put(100, 80){\oval(100,70)} % Relays \put( 60, 55){\usebox{\relay}} \put( 60, 85){\usebox{\relay}} \put(120, 85){\usebox{\relay}} % Connections between relays \put( 80, 95){\line(1,0){40}} \put( 70, 75){\line(0,1){10}} \put( 80, 65){\line(5,2){50}} % Phones and connections \put(0,0){\usebox{\threephones}} \end{picture} \end{center} \noindent A retrieval relation between the abstract and concrete descriptions must be provided. The non-determinism in the formal abstract description (\ie all occurrences of $\nondetchoice$) may be removed by providing more information about the implementation of the telephone exchange. The implementation can be formally proved to be a refinement of the abstract description using formal rules provided by Jifeng He of the PRG. The question and answer session elucidated a number of points: \nopagebreak \begin{itemize} \item Transient states are not retrieved --- only stable states are considered. \item Deadlocks and live-locks must be checked. Jifeng's rules ensure that these are avoided. \item Divergence must also be avoided --- an infinite sequence of events should never be hidden. \item The $Connect$ demon can connect two or more requests in an arbitrary order. \end{itemize} \subsection{Z Refinement, Carroll Morgan} Carroll Morgan, a lecturer at the PRG, described a method of refinement from an abstract specification (\eg something akin to \Z) into a programming language. The notation used is not in the framework of the current \Z\ notation. What is needed is a single notation which at its most abstract allows the use of schemas\footnote[1]{Almost} and at its most concrete allows executable programs\footnotemark[1]. A calculus of {\em refinement} is introduced which operates across this notation uniformly. At the abstract level, the {\em domain} of each operation is calculated and written explicitly, so that it need not be calculated again. The {\em changing variables} are indicated explicitly, so that unchanging variables need not be indicated. \Eg \begin{schema}{EXAMPLE} x,y,x',y' : T \where \varphi(x,y,x') \\ y' = y \end{schema} \noindent translates to \nopagebreak \[ x:[(\Exists{x'} \varphi(x,y,x')) , \varphi(x,y,x')] \] \noindent The initial $x$ indicates the changing variable(s). The rest of the statement indicates the precondition (or domain) and postcondition: $[pre,post]$. At the concrete level, Dijkstra's language of {\em weakest preconditions} is used to describe executable programs. This is a very simple language: \nopagebreak \begin{tabbing} XXXXXX \= Do anythingXXXX \= \kill \> Do nothing \> $\SKIP$ \\ \> Do anything \> $\ABORT$ \\ \> Assign \> $x := E$ \\ \> Sequence \> $P ; Q$ \\ \> Conditional \> $\IF\ G_{1} \THEN S_{1} \ALT \ldots \ALT G_{n} \THEN S_{n}\ \FI$ \\ \> Iteration \> $\DO\ G_{1} \THEN S_{1} \ALT \ldots \ALT G_{n} \THEN S_{n}\ \DO$ \end{tabbing} An important feature of the language is that it is non-deterministic. If two or more guards on a conditional statement are true then any one of the corresponding guarded statements could be executed. However the language is readily translated into imperative programming languages such as Pascal, FORTRAN, etc. The refinement calculus $\refinement$ has a number of rules or laws; the following are some examples: \nopagebreak \begin{itemize} \item The precondition may be weakened: \nopagebreak \[ w:[\varphi,\psi] \refinement w:[\chi,\psi] {\rm\hspace{1.0in} if\ } \varphi \THEN \chi \] \item The postcondition may be strengthened: \nopagebreak \[ w:[\varphi,\psi] \refinement w:[\varphi,\chi] {\rm\hspace{1.0in} if\ } \chi \land \varphi \THEN \psi \] \item An assignment statement may be introduced: \nopagebreak \[ w:[\varphi[E/w'],\psi] \refinement w:=E \] \item Sequential composition ($;\!$) provides ordering of statements: \nopagebreak \[ w:[\varphi,\psi] \refinement w:[\varphi,\chi']\ ;\ w:[\chi,\psi] \] $\chi$ is an intermediate state. An interesting point is that this refinement is possible even if $\chi = false$. \item If at least one guard is $true$ then the $\IF$ statement may be introduced: \nopagebreak \[ w:[(\bigvee i.G_{i}) \land \varphi,\psi] \refinement \\ \IF \\ \t1 (\ALT i.\ G_{i} \THEN w:[G_{i} \land \varphi,\psi]\ ) \\ \FI \] \item Finally, the $\DO$ statement can be introduced for iteration: \nopagebreak \[ w:[I,I \land \lnot G] \refinement \\ \DO \\ \t1 G \THEN w:[I \land G, I \land 0 \leq V' < V] \\ \OD \] $I$ is the invariant and $V$ the variant. \end{itemize} Here is a simple example which calculates the absolute value of a natural number. Note that parts within $[\ldots]$ are the parts which are left the be refined. \begin{schema}{ABS} x, x' : \nat \where x' = |x| \end{schema} \noindent transforms to \nopagebreak[3] \begin{tabbing} \htab $\refinement$ \= \kill \> $x:[true,x'=|x|]$ \end{tabbing} \noindent First the precondition is weakened: \nopagebreak \begin{tabbing} \htab $\refinement$ $x:[(x \leq 0) \lor (x \geq 0), x'=|x|]$ \end{tabbing} \noindent Next the $\IF$ rule is applied: \nopagebreak \begin{tabbing} \htab $\refinement$ \= $\IF\ $ \= $x \leq 0 \THEN x:[x \leq 0, x'=|x|]$ \\ \> $\ALT$ \> $x \geq 0 \THEN x:[x \geq 0, x'=|x|]$ \\ \> $\FI$ \end{tabbing} \noindent The preconditions can be transformed: \nopagebreak \begin{tabbing} \htab $\refinement$ \= $\IF\ $ \= $x \leq 0 \THEN x:[-x=|x|, x'=|x|]$ \\ \> $\ALT$ \> $x \geq 0 \THEN x:[x=|x|, x'=|x|]$ \\ \> $\FI$ \end{tabbing} \noindent Now the specification can be made totally executable: \nopagebreak \begin{tabbing} \htab $\refinement$ \= $\IF\ $ \= $x \leq 0 \THEN x:=-x$ \\ \> $\ALT$ \> $x \geq 0 \THEN \SKIP$ \\ \> $\FI$ \end{tabbing} \noindent It can also be made deterministic: \nopagebreak \begin{tabbing} \htab $\refinement$ \= $\IF\ $ \= $x \leq 0 \THEN x:=-x$ \\ \> $\ALT$ \> $x > 0 \THEN \SKIP$ \\ \> $\FI$ \end{tabbing} \noindent Informally, this can be refined into a typical imperative programming language as: \nopagebreak \[ \keyword{if}\ x \leq 0\ \keyword{then}\ x := -x\ \keyword{end} \] The refinement process above is not mechanical in that invariants, etc., must be found. The designer must decide which development step to take at each stage. However the refinement rules give a rigid and formal framework for this. Next Carroll talked about {\em data refinement}, a transformation which systematically replaces one data type (the abstract) by another (the concrete) throughout a program. The program structure is preserved. Given abstract variables $a$ and concrete variables $c$, we can define an abstraction invariant $I(a,c,g)$. The data refinement $\dataref$ can then be calculated as follows: \nopagebreak \[ a,x:[\varphi,\psi] \dataref c,x[(\Exists{a} I \land \varphi), (\Exists{a} I \land \psi)] \] \noindent This is always true --- there are no proof obligations. However some subsequent algorithmic refinement is usually required. It is possible to have intermediate steps. The refinement is transitive. \newpara John Nicholls concluded the session by noting that there will be a workshop on refinement at York University on 7th/8th January 1988 at which several members of the PRG (and others working with \Z) will be giving presentations. \section{Prototype FORSITE Tool Demonstration} About 30 people attended a demonstration by Joy Reed and Jane Sinclair of the FORSITE prototype syntax and type checking tool running on a Sun workstation at the PRG after lunch. \section{Z Education} The possibility of a course on ``{\em Z for Specifications\/}'' based on the MSc.\ and industry courses at the PRG was discussed by John Nicholls. The objective is to produce an industry course to introduce the use of \Z\ to specify software systems. It will be fully documented, with foils, exercises, course notes, etc. At present, Anthony Hall, John Nicholls, Joy Reed and Jim Woodcock are involved in designing and writing the material for this course. The following schedule has been drawn up: \nopagebreak \begin{itemize} \item January 1988 --- all modules specified. \item Mid 1988 --- draft course material complete (pilot courses). \item Late 1988 --- publication (format to be decided). \end{itemize} \noindent The (one week) course structure will be as follows: \nopagebreak % See p114, LaTeX book. \newcounter{alphcount} \begin{list} {\Alph{alphcount}.}{\usecounter{alphcount} \setlength{\rightmargin}{\leftmargin}} \itemsep=0pt \item Motivation. \item Discrete mathematics (optional, background information). \item Basic \Z. \item Managing projects using formal methods. \item Extended case study. \item Workshop (1--1\half\ days writing \Z). \item \Z\ proofs. \item \Z\ refinement (introduction to another course). \end{list} \noindent The course material will be prepared for class room use rather than computer based training. \section{Z Tools and Environments} This session included two presentations on machine assistance for \Z. These contrasted the use of \Z\ in a sophisticated and a simple environment. \subsection{The FORSITE Project, Dave Bosomworth} Dave Bosomworth of Racal gave an overview of the FORSITE project. This is an Alvey project running from August 1985 to March 1989. Racal Research Ltd, System Designers, Surrey University and the PRG are involved in the project. The background to the project was an Alvey Demonstrator Project involved in producing \Z\ specifications over 6--9 months. This found the need for tools to aid organization and to do syntax/type checking. Names could be remembered in the head for only around two pages whilst reading specifications. The project objectives were to produce a \Z\ toolset and handbook. In the course of doing this, the syntax of \Z\ should be tied down. To date, an evaluation system including a parser, type checker, WYSIWYG editor (QED) and printing facilities has been produced. This has users at four industrial sites (Plessey/Praxis/ICL/IST) and three academic sites (Edinburgh/York Universities and Sheffield Polytechnic). The real requirements for \Z\ tools is still a subject of debate. The project has not answered any hard theoretical questions so far (\eg refinement and proofs). It is hoped that these will be addressed in the future, particularly in regard to large examples. The plans for the project include work on proof systems (at present the {\bf b} tool is used), transformation systems, development methods (there are no set steps at present) and better tools. The FORSITE system runs on Sun workstations. It is mostly written in C, although the type checker is in the functional programming language ML. % Tools for Z documentation \subsection{Z on an IBM PC --- the Issues, Jonathan Moffett} Jonathan Moffett of Imperial College recently attended a \Z\ course given by the PRG. Following the course, he raised the question of providing support for producing \Z\ documents on an IBM PC. He noted that \Z\ is text rather than graphics. Therefore a word processing package rather than a graphics package is all that is needed. The special (non-ASCII) characters in \Z\ can be reproduced using special fonts. Additionally, the special characters can be keyed in on a normal keyboard. \Z\ is designed for large specifications. Therefore the special characters need to be stored in an easily handled form. Jonathan made the following (not yet implemented) proposals. \begin{itemize} \item The special characters should be keyed using mnemonics (see {\em Z: Grammar and Abstract and Concrete Syntaxes} by Steve King et al.). \item These mnemonics should be post processed using a macro processor. This processing is not necessary to be able to read the document whilst working on it. It is simply desirable to produce a better end product. \end{itemize} The \Z\ character set may be split up into a number of groups on the IBM PC. There are the standard alphanumeric characters together with characters such as \nopagebreak \[ (\ )\ [\ ]\ \ldots \etc \] \noindent which may be keyed directly on the IBM keyboard. There are standard letters but in different fonts. \Eg \nopagebreak \[ \aleph\ \Re\ \ldots \etc \] \noindent Note that these are Gothic rather than baroque fonts! Unfortunately, the more normal $\nat$, $\real$, \etc are not available on the IBM PC. The extended graphics character set can be used for lines, boxes and $\theorem$. The mathematical font characters (for the Apple Laserwriter) cover the Greek letters and \nopagebreak \[ \forall\ \exists\ \defs\ \neq\ \neg\ \lor\ \land\ \implies \ldots \etc \] \noindent Special characters are needed for ``funny'' arrows and \nopagebreak \[ \dres\ \rres\ \ndres\ \nrres\ \project \ldots \etc \] Programmers are used to mnemonics. However John Nicholls noted that most people prefer seeing mathematical symbols where these are appropriate. They are easier to read and more compact. An alternative solution is to use PC \LaTeX. {\sc Lexx}, a live parsing editor, has a dynamic parser and could provide another solution. There are also word processing packages to run on the PC for as low as \pounds20 which provide mathematical fonts. Jonathan Moffett's system cost around \pounds700 including a printer. With an Epson laser printer, the cost would rise to about \pounds2000. \section{Z User Presentations} A number of short presentations by \Z\ users (mainly from industry) were given in this session. These provided varied examples of the way \Z\ can be and has been applied to different problems. \subsection{British Aerospace, Brian Hepworth} Brian Hepworth of the Software Reliability group in the Military Aircraft Division at Warton presented the use of \Z\ in control systems. Currently there are three users of \Z\ in the company. Most users of \Z\ are likely to be ``naive'' users (systems engineers) using ``simple'' \Z. The difficult parts will be undertaken by a small group of experts. Brian gave an example of a control system, which he noted was quite similar to Jim Woodcock's telephone exchange. Since the system is distributed, it can be easily split up for different teams. Previously CORE has been used at the upper level of design. It is hoped that \Z\ will replace this. Many of the operations are stateless, with only inputs and outputs --- the state is held externally. Sometimes it is necessary to introduce state to model history sequences. Functions specified by the \Z\ experts can be defined to handle these simply. In the future it may be convenient to use some of the features of CSP for this. \subsection{IBM, Peter Collins} Peter Collins of IBM, Hursley Park, started by saying he was going to tell a ``story of unstable (\ie changing) software rather than unstable aircraft!'' He presented the experience of using \Z\ on the IBM Customer Information Control System (CICS). This is a large transaction processing system which is an extension of the operating system. It has been developed at Hursley and has many thousands of users worldwide. It consists of well in excess of half a million lines of code, written in a mixture of assembler and high level language. It has had many years of continuous development using a well established development process. The use of \Z\ at Hursley started as a joint project between the PRG and the CICS development team in 1981. The objective was to study the applicability of formal specification techniques to the development of CICS. Initially case studies where undertaken using the \Z\ specification language. In 1984 it was decided to use \Z\ in the CICS, first in pilot projects and then for mainline development. The alternative possibility (CDL) was dropped and the complete development process has been based on \Z. Twenty developers have written about 2000 pages of \Z\ specifications. Subsequently, around 90,000 lines of code have been written. Coding is now complete and testing is well underway. This has shown that the quality is significantly higher than when using traditional development methods. About a third of a release of CICS has been produced using formal techniques. Formal methods have been used for the specification and design of selected CICS components. These provide both new functions and reimplementation of existing functions. Standard \Z\ has been used for component specification. An extended version of \Z\ has been used for component design. This includes Dijkstra's guarded command language to allow the specification of procedural design. Its mathematical basis permits formal reasoning. The development process has been changed to accommodate the use of formal methods. Design Review 0 ({\bf DR0}) has been introduced to review the \Z\ specifications. At this stage the interface is reviewed by potential users. Quite a few problems are removed at this point. The {\bf I0} and {\bf I1} design inspections have been modified to take account of \Z. {\bf I0} is an informal check that the design is a correct refinement of the {\bf DR0} specification. There is no formal proof of refinement. This is very expensive without machine assistance and is not believed to be cost effective at present. The work at the PRG has been mainly based on case studies of real examples from CICS. These have exposed new kinds of problems. They have demonstrated the feasibility of using formal methods to the potential users and their management. They also provide examples for others to follow. There is a user resistance to the introduction of formal techniques. Using real examples is more impressive than the simple examples found in much of the literature. Even so, some management faith is required. The specification stage is longer and the coding stage much shorter when using formal techniques. It is possible for managers to lose their nerve and revert to traditional methods. The case studies were followed by pilot projects. These involved small motivated groups, giving rise to local experts at IBM. As a result, rules and guidelines were generated for other users. Additionally, these projects helped identify other requirements. A number of courses have been developed at IBM. A two week Software Engineering Workshop uses SDTL rather than \Z. However there are now a number of \Z\ courses provided by John Wordsworth and others of the Software Engineering group at Hursley: \nopagebreak \begin{itemize} \item {\em Z Specification course} --- originally provided by the PRG but revised by IBM. \item {\em Z Refinement course} --- the refinement of \Z\ specifications to design and code. \item {\em Z for Readers course} --- understanding other people's specifications. \item {\em Z Overview} --- brief overview of \Z\ for managers. \end{itemize} A number of tools for \Z\ have been developed at IBM Hursley. The initial tools were developed by the CICS developers. \Z\ documents may be prepared and viewed on an IBM 3279 display. Special \Z\ characters are entered using mnemonics and are then translated. Subsequently documents may be printed using a Document Composition Facility on an IBM 3800. The system consists of terminals and a mainframe computer. It would be expensive to convert to IBM PCs. There is also a powerful cross-reference program which is very useful for large specifications. Despite the limited machine assistance, there have not been a lot of complaints about the lack of more sophisticated tools. It is important in a commercial environment to have a stable notation. Researchers naturally wish to improve and change the notation, so there is a potential conflict of interests. No agreed standard for \Z\ existed at the start of the project; it is a good thing that the PRG is now standardizing \Z. As part of the project a precise and stable base language has been defined. This includes a formal syntax to be used as the basis for tools such as type-checkers. A {\em Z User Manual} has also been produced. This gives an informal guide to the notation with examples of use. There is a need for a manual such as this. Both Mike Spivey's manual (the {\em Z Reference Manual\/}) and one like this are useful and complement each other. Another important consideration is a standard for representing \Z\ documents; standards become more important as the number of \Z\ users increases. Users at IBM have been impressed by the simplicity and elegance of \Z. Users especially like the ability to compose large specifications from small parts. Better interfaces have resulted and the specification of existing interfaces has showed up their weaknesses. \Z\ has proved to be a tool for ideas. Better informal documentation has resulted. \Z\ specification has been used in testing --- pre/post-conditions and invariants can be checked. However this can use more code than is actually being checked. The formal mathematical nature of \Z\ has not proved a major problem in acceptance by programmers. Indications are that more problems are found during early stages. Documentation is more complete and easier to inspect. The overall quality of software and documentation is much improved. One minor problem has been that some users find it difficult to find the right level of abstraction. If a programmer knows the internal workings of a system, he often finds it difficult not to think about these when producing an abstract specification. \subsection{Plessey, David Cooper} David Cooper of the Formal Methods Group at Plessey Research, Roke Manor gave a presentation of a short paper entitled {\em Some Notes on the Use of Z}. This three page paper is included with this Proceedings. The paper presents some difficulties they experienced in the use of \Z\ for large specifications but David is still committed to \Z. Perhaps part of the problem may be that the team has been trying to come to terms with the use of \Z\ whilst working on a very large project. It is possible that a more gentle introduction to the practical use of \Z\ may be desirable. More contact with the PRG could also help to solve some of these problems. Several instruction sets have been specified at the PRG without many of the problems covered in the paper. (The Motorola 6800 8-bit microprocessor instruction set has been completely specified and is available as a PRG monograph. Partial specifications of the Motorola 16-bit 68000 and the {\sc inmos} Transputer have also been produced.) The project has relied heavily on the FORSITE tool. This ensures a strictly type-checked \Z\ specification but also enforces notational limitations since the tool does not support all the features of \Z\ and will not allow non-standard notational extensions. The IBM CICS project has demonstrated that it is not necessary to have such a tool to successfully produce large specifications. \subsection{RSRE, Chris Sennett} Chris Sennett of the Royal Signals and Radar Establishment (RSRE) at Malvern is concerned with security problems in computer systems. He is involved in the Hindsight Project which is working on a syntax and type checker for \Z\ at RSRE. The main part of the talk was about the translation of the mathematical content of a paper on {\em separability} by John Rushby of Newcastle University into the \Z\ notation. This process simplified formulae and aided understanding. The proof steps were laid out so that they were potentially machine checkable. Chris commented that it could be desirable to have a number of equivalent definitions in the \Z\ mathematical toolkit. Different definitions could be aimed at ease of understanding on the one hand and ease of use in proofs on the other. In summary, the use of the \Z\ language help specify precisely what {\em separability} is about and increased understanding of the problem. Using \Z\ and English in parallel is very useful --- the \Z\ can aid the understanding of the English! The \Z\ specification produced during the exercise was very compact. The original paper was 17 pages long; the version translated into \Z\ by Chris consisted of 25 pages. \section{Research Directions} Professor Tony Hoare of the PRG presented his view of research at the PRG in the future. He started his talk with an entertaining analogy of a geologist and a car driver. The geologist (researcher) searches for oil (knowledge) and the car driver (industrial user) needs petrol (methods). Even if a petrol pump (\Z\ user group?) is available, this must still be supplied with petrol. What is basic research? It is as far removed from industry as geology is from the car --- but the latter still depends on the former. Basic research is like mountaineering; we do it ``because it's there.'' Basic research clarifies the structure of a disipline, and permits collaboration of specialists working in adjacent areas. Some mathematical research foundations are: \nopagebreak \begin{itemize} \item Logic \item Algebra \item Type theory \item Category theory \end{itemize} \noindent Some computing paradigms for which these can or could be useful include: \nopagebreak \begin{itemize} \item Hardware \item Functional programming \item {\em Prolog\/}ical programming \item Object-oriented programming \item Distributed systems \end{itemize} Sometimes it is useful to mix paradigms (\eg assembler within a high level program). How can we deal with this? How do we check interfaces between paradigms, where many bugs can lurk? Currently some machine assistance for proofs is available. \Eg \begin{itemize} \item Boyer-Moore --- 15 years work. \item LCF, Edinburgh --- again, 15 years work. \item HOL, Cambridge. \item Veritas. \item LF, Edinburgh. \end{itemize} Each of these presents formidable problems and expense to the practical user. Basic research may reveal new directions for progress. There are also a number of methods other than \Z: \nopagebreak \begin{itemize} \item UNITY --- Chandy and Misra at Austin. \item VDM --- an acceptable alternative! \item Nuprl --- Martin-Lof type theory. \item Projet Formel --- 2nd order logic and category theory. \end{itemize} It would be a worthwhile research project to prove a complete system at a number of levels using such tools and methods: \nopagebreak \begin{itemize} \item Compiler/loader \item Operating system \item Architecture \item Logic design \end{itemize} \noindent Human readable proofs would be acceptable. The interfaces between levels should also be proved. Computational Logic Inc., in Austin, Texas, are attempting to do something like this with 12 people and Symbolics machines. We should also try to do this in Europe as an ESPRIT project. There is a lot of skill in this area in Europe, but it needs coordinating. \newpara A short discussion then followed. Question: ``Are reusable libraries a suitable topic for basic research?'' The term {\em reusable} has been a buzz-word for 25 years. Such libraries must be as carefully designed as a range of cars and hence need a great deal of effort to produce. Standard functions such as {\tt sin} and {\tt cos} are already well known and understood. What equivalents do we need for computer systems? \Z\ has isolated a number of common concepts and is sufficiently abstract to describe similarities between systems. But suppose we had a reusable library. How would we use it, index it, and so on? This would have to be done by a very large company with a lot of resources. Question: ``How do we deal with probability and is this a good research topic?'' Yes --- Mike Reed at the PRG is working on a probabilistic version of CSP. However timed CSP took a long time to develop and a probabilistic version may take even longer. \section{Future Work} John Nicholls asked the audience if they would be interested in the formation of a \Z\ User Group. This would place \Z\ in a wider arena. John Wordsworth of IBM suggested that it might be formed as a specialist group under the auspices of the British Computer Society (BCS). Interest was expressed by the audience. Anyone interested should contact John Nicholls at the PRG. \newpara John closed the meeting by thanking the speakers, especially those during the \Z\ user presentations which reflected the wide applicability of \Z. Finally he thanked Emma Sowton of the PRG for arranging the administrative side of the meeting so efficiently. \section{Acknowledgements} Thank you to all the speakers for making the 1987 \Z\ Users Meeting a worthwhile day for all the participants. A special thank you to all those who gave copies of their foils and notes to aid the production of this record. Please accept the author's apologies for any mistakes in the transcription from verbal to written form. John Nicholls and other speakers from the PRG gave valuable comments on the first draft of the Proceedings. Finally, thank you to the audience for making the meeting a success, and hopefully a continuing annual event. \end{document} *************************** END OF Z FORUM 3.1 **********************