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!daemon From: zforum@uk.ac.oxford.prg Newsgroups: zforum Subject: Z Forum 5.2 Message-ID: <9003051257.AA20009@topaz.prg.ox.ac.uk> Date: 5 Mar 90 13:26:21 GMT Date-Received: 5 Mar 90 13:27:12 GMT Lines: 254 Original-Date: Mon, 5 Mar 90 12:57:53 GMT 5th March 1990 Z FORUM Volume 5 Issue 2 -------------- ------- ---------------- Today's Topics -------------- Formal Semantics in Z Z bibliography SafetyNet '90 ------------------------------------------------------------------------------- From: paulb@uk.ac.york.minster Date: 13 Feb 1990 10:41:51 GMT Subject: Formal Semantics in Z I've recently started on producing a formal semantics for the Linda programming language in Z. Z was chosen mainly for pragmatic reasons - there is a considerable amount of Z experience at York, and we have our own Z type checker running under troff (zork, written by Ian Toyn). I have experienced a number of problems with the specification which I have been unable to resolve to my satisfaction, even with the help of a number of experienced Z users. I would be very interested in hearing the views of the Z Forum. I ought to start by saying that I am not a Z hacker, and this is the first time I've seriously tried to use Z. It is therefore entirely possible that I've overlooked something trivial, and the solution is obvious. I don't however believe this to be the case. I won't attempt to describe Linda in any great detail here, but there are a couple of references at the end for anyone interested. Linda is not a complete language in its own right, but needs to be embedded in a `host' languge. Linda provides inter-process communication, transforming the host language into a parallel programming language (e.g. C may be transformed into C-Linda, Lisp into Lisp-Linda etc.). The main abstraction in Linda is `Tuple Space', which is bag of tuples (NB when I use the word `tuple' here, I am referring to tuples in the Linda, rather than the Z sense). Processes communicate via Tuple Space by adding and removing tuples. A tuple is a sequence of typed fields. A field may contain a value of that type (an actual), or may contain the special value `NULL' (a formal). Tuples may be partitioned into two sets. Passive tuples are tuples containing only data. Active tuples may have processes as elements (this is where the problems start). Processes may manipulate Tuple Space, and I am modelling this by having processes request events of Tuple Space. Associated with each event is a value (e.g. a process may add a tuple to Tuple Space by requesting an `out' event. The value associated with this event is the tuple to be added to tuple space). The basic structure of the specification is therefore (in a BNF-ish notation) Tuple ::= Element {Element} Element ::= (Type, Value) Value ::= LangVal | Process LangVal ::= NULL | ... Process ::= (ProcID, Event) Event ::= (EventName, EventValue) EventName ::= out | in | ... EventValue ::= LangVal | Tuple ^^^^^ This is the problem. The structure of Tuple Space is inherently recursive; Tuples may contain processes, and processes may manipulate Tuples, which may contain processes ... ad infinitum. My first, naive, attempt ran up against this brick wall very soon, and I thought that I would have to abandon the whole thing. Reading through the reference manual specification of a tree structure gave me the following idea; using generic schemas to allow me to define a tuple in terms of a process, even though I hadn't defined a process yet. This took the following form; ==TupleElement[ElemValues]=== | Type : TypeName | Value : ElemValues ----------------------------- ==Tuple[ElemValues]========================= | Elements : seq TupleElement[ElemValues] -------------------------------------------- Alphabet ::= inEvent | outEvent | ... ==Process[EventValues]=== | ID : ProcID | Event : Alphabet | Value : EventValues ------------------------- Values ::= TupleVal << Tuple[Values] >> | ProcVal << Process[Values] >> | LangVal << ... >> | NULL The problem with this is that I now have to define what I mean by a valid process (as a process may not contain other processes, nor may it give the value NULL as an EventValue). | ValidProcess _ : powerset Process[Values] |------------ | forall p : Process[Values] . | ValidProcess p <==> | p.Value notmem ran ProcVal and | p.Value /= NULL and | ... Unfortunately, I now need to define a valid tuple, as a tuple may only contain valid processes. I then need to define a valid valid process, as a process may only manipulate valid tuples, then a valid valid tuple etc. etc. Another complaint about the structure above is that I consider it an `inelegant' solution. I am forced to use generic schemas when there is nothing generic about the things I am defining. Also Values is far too general; the only elements common to both an `ElemVal' and an `EventVal' are those in `LangVal'. It occurred to me that there would be no problem if Z provided a "forward" operator, which would allow me to define tuples in terms of processes before I had defined a process. The argument against a forward operator is, as I understand it, that Z should not allow recursion. As far as I can see however recursion may be introduced by using generic schemas as I have done above. Unfortunately it is a limited form of recursion, which is not capable of handling the structure I wish to define. Any suggestions anyone? +--------------------------+---------------------------------------------+ |Paul Butcher | JANET: paulb@uk.ac.york.minster | |Dept. of Computer Science | EARN: paulb@minster.york.ac.uk | |University of York | UUNET: ..!uunet!mcvax!ukc!minster!paulb | |York YO1 5DD ENGLAND | ARPA: paulb%york.minster@nss.cs.ucl.ac.uk | |Tel: (0904) 432760 | Alternative address: | | (+44 960) 432760 | PRAB1@uk.ac.york | +--------------------------+---------------------------------------------+ ------------------------------------------------------------------------------- From: Jonathan.Bowen@uk.ac.oxford.prg Date: Thu, 22 Feb 90 12:18:46 GMT Subject: Z bibliography The following files on the PRG archive server have been updated since the Z Users Meeting in December: zbib Unix refer version of Z Bibliography (source version) zselectbib Selection from above bibliography zbib.roff Formatted version of "Z Bibliography" zselectbib.roff Formatted version of "Selected Z Bibliography" zbib.bib BibTeX database of Z Bibliography (generated from zbib) zbib.tex LaTeX source to generate Z Bibliography from zbib.bib These may be retrieved by sending a command such as send z zbib zbib.bib (for example) in an electronic mail message to (on JANET). For more information on the archive server, send a command of "help". -- Jonathan Bowen, Programming Research Group, Oxford University. ------------------------------------------------------------------------------- From: Ruaridh Macdonald Date: Fri, 2 Mar 90 14:07:32.99 GMT Subject: SafetyNet '90 Call for Papers and other contributions SAFETYNET '90 ------------- Second Conference on the use of FORMAL METHODS for critical computer systems development. Royal Signals and Radar Establishment. Malvern, Worcestershire, England. Tue. 16th and Wed. 17th October 1990. The conference aims to provide a forum for the dissemination of knowledge and experience of Formal Methods, also for discussion of developments and future trends in application and use. A discussion session will be a key feature of this year's conference. Evidence and argument will be invited on the following question: Are Formal Methods sufficiently developed and in a state fit to be trusted in the development of critical computer systems? CONTRIBUTIONS Offers are invited by the Programme Committee for: - Papers - Tutorials - Places on Discussion Panel TOPICS - Experience in the use of Formal Methods in the development of critical computer systems - Specific techniques - Formal approaches to requirements analysis - Formal notations for systems description - Verifiable designs - Proof methods - Fault tolerant design - Tools supporting the use of Formal Methods - Theories - Relevant professional attitudes and legal issues - Standards developments - etc. DEADLINES Last Dates Receipt of abstracts of papers 6th April 1990 Receipt of synopses of tutorials 6th April 1990 Application for places on Discussion Panel 6th April 1990 Notification of acceptance (provisional) 27th April 1990 Receipt of full texts 29th June 1990 Notification of acceptance (final) 13th July 1990 Please send offers of contributions and requests for Conference Registration Forms to: SafetyNet '90 Conference, VIPER Technologies Ltd., P.O. Box 79, 19 Trinity Street, Worcester WR1 2PX England Tel. 0905 611512 Fax. 0905 612829 ****************************** END OF Z FORUM 5.2 *****************************