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: Ruaridh Macdonald Newsgroups: zforum Subject: Z Forum 5.3 Message-ID: <9005141204.AA15155@topaz.prg.ox.ac.uk> Date: 14 May 90 12:47:22 GMT Date-Received: 14 May 90 12:48:05 GMT Lines: 503 Original-Date: Mon, 14 May 90 12:25 GMT 3rd May 1990 Z FORUM Volume 5 Issue 3 ------------ ------- ---------------- Today's Topics -------------- Language Semantics Operational Semantics of a Distributed O.O.L. in Z The Queen's Award for Technological Achievement Z Meetings ----------------------------------------------------------------------------- From: Anthony Hall Date: Mon, 26 Mar 90 19:30:47 BST Subject: Language Semantics Formal Semantics in Z --------------------- In Z Forum 5.2 Paul Butcher posed a problem to do with the use of Z for the formal semantics of a programming language. Problems of this sort seem to arise quite frequently. Their solution is quite straightforward but it is not at first obvious and I as well as many others have had difficulty seeing the solution. Therefore, although Paul has subsequently solved the problem, I thought it worthwhile to contribute a suggested solution to Z forum. Here is a shortened version of the problem: > >I've recently started on producing a formal semantics for the Linda >programming language in Z. >... >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. >.... >The problem with this [the attempted solution] > 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). >.... >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. >.... >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. The key here is the statement "Z should not allow recursion". There is clearly a problem with the existing descriptions of Z if they give this impression. Z very definitely *does* allow recursion. It does not allow use before declaration, however. That is, types must be introduced before they are used. Nevertheless, once a type has been introduced it may be constrained by any number of subsequent predicates. For example, consider the simple declaration [Error] | tooBig, tooSmall : Error |------ | tooBig /= tooSmall This bit of Z constrains `Error' to have at least two elements. I think this is essentially equivalent to the `forward' construct that is suggested. These predicates may use any logical constructs at all including recursion. Of course, if they *do* use recursion, you have a proof obligation to show that there is a solution to the recursion equations you are using. As an important aside: you have to remember that the semantics of Z is set-theoretic, and so your equations must have a solution in set theory. So for some quite simple programming languages you will not be able to express their semantics in Z; you will need a domain-theoretic model. Most obviously, if you try something like [Function] | meaning : Function >--> (Function >-|-> Function) to try to describe a language which includes higher order functions you have written something which is syntactically perfect Z but has no model in set theory. However, as far as I can see Linda does not pose this problem. End of aside. There is one apparent exception to the rule of declaration before use in Z, and that is the recursive free type definition, such as that for a tree in the reference manual. Now in fact free type definitions in Z can be regarded as syntactic sugar. For example Value ::= lv <> | pv <> is actually short for [Value] | lv: (LangVal >-> Value) | pv: (Process >-> Value) |---------------------------------- | <(\ran lv), (\ran pv)> \partition Value Although Z does not allow *mutually* recursive free type definitions, it certainly *does* allow mutually recursive constraints on already introduced types. So one can write specifications similar to the above but with several mutually recursive relationships between types; the only thing you don't have available is the syntactic sugar of the free type definition. Using this basic idea, I think there are several ways of defining the semantics of Linda. Solution 1 is the most direct translation of the BNF definition Solution 1 ---------- The following is an edited transcription of the output from fuzz, so I can guarantee that it is type-correct! Start by defining the most basic types we need: LangVal ::= NULL | others EventName ::= out | in | etc [Type] Now here is the `trick'. We would like to write something like Value ::= lv<> | pv<>. Unfortunately we can't because we don't yet know what `Process' is. But we can introduce Value now and constrain it later. [Value] You can define record types like Element as cartesian product types or as schemas. I've chosen schemas, but you could have Element == Type x Value if you prefer. schema Element type: Type value: Value end We can now equate tuples with sequences of elements Tuple == (seq Element) [ProcId] EventValue ::= le << LangVal >> | te << Tuple >> schema Event name: EventName value: EventValue end schema Process id: ProcId event: Event end Now we can complete the definition of Value by adding the constraints | lv: (LangVal >-> Value) | pv: (Process >-> Value) |------------------------------------------------ | <(\ran lv), (\ran pv)> \partition Value Finally, we can define the notion of validity. We have all the types, so we can be as recursive as we like. | validProcess: (P Process) | validTuple: (P Tuple) |------------------------------------------------- | validProcess = | { p: Process | p.event.value in | (le (| (LangVal \setminus {NULL}) |) \cup | te (| (validTuple \setminus | { t: Tuple | (exists e: (\ran t) @ e.value in (\ran pv)) } | ) | |) | ) | } | | validTuple = | { t: Tuple | (forall e: (\ran t) | @ e.value in ((\ran lv) \cup pv (| validProcess |))) | } That is, a valid process has event values which are LangVals, but not NULL, or they are valid tuples excluding those containing processes. A valid tuple is one whose event values are Langvals or valid processes. (I may have misunderstood the exact conditions here, but I hope the idea is clear) I think there is a Solution 1a in which the validity conditions are incorporated into the type definitions. In other words instead of defining validTuple, you incorporate the predicate into the definition of Tuple, and similarly for validProcess. However, the margin is a bit small to write this solution :-) Which solution you choose depends on whether you wish to consider the possibility of *invalid* tuples and processes: if they can never arise, solution 1a is better, but if they are constructible and need to be checked for, then solution 1 is what is needed. Solution 2 ---------- Solution 1 is what one might term a `value-based' solution, in that it considers tuples to be values - in this case sequences of elements. There is an alternative approach which is often more appropriate, although I have no idea whether it is in this case. That is what one might call an `object-based' approach, in which one considers a tuple to be an object in its own right, which in some sense `contains' a sequence of elements. You can tell which solution is more appropriate by asking whether it makes any sense to *change* a tuple. If it does, then tuples have existence beyond the sequence of elements they contain, and you should use an object based model; if it makes no sense, then the value-based model is correct. The object-based solution has a completely non-recursive type structure. Tuples are introduced right at the beginning as a completely abstract type; then their possible contents are built up, and finally the state of tuple space is modelled as a mapping from tuples to their contents. I haven't included the validity constraints here (that margin again) but they would be included as predicates in the tuple space schema. [Tuple] [Type] LangVal ::= NULL | others [ProcId] EventName ::= out | in | etc EventValue ::= le << LangVal >> | te << Tuple >> schema Event name: EventName value: EventValue end schema Process id: ProcId event: Event end Value ::= lv << LangVal >> | pv << Process >> schema Element type: Type value: Value end And finally the state of the system at any time is represented by an ordinary Z state schema. schema TupleSpace tuples: (Tuple -+> (seq Element)) end ----------------------------------------------------------------------------- Date: Mon, 23 Apr 90 14:18:15 +0200 Subject: Operational Semantics of a Distributed O.O.L. in Z From: Marc Benveniste I have specified in Z the operational semantics of a parallel object-based language, super-set of Modula-2. My work is available as an english written IRISA's technical report. The specification is type-checked with M. Spivey's "fuzz". The report will be soon available as an INRIA publication. "Operational Semantics of a Distributed Object-Oriented Language and Its Z Formal Specification" Marc Benveniste Publication Interne no. 532, Avril 1990. IRISA Campus de Beaulieu F-35042 Rennes Cedex FRANCE. ----------------------------------------------------------------------------- Date: Sat, 21 Apr 90 00:01:00 BST From: Geraint Jones Subject: The Queen's Award for Technological Achievement 1990, INMOS and Oxford ``Her Majesty the Queen has been graciously pleased to approve the Prime Minister's recommendation that The Queen's Award for Technological Achievement should be conferred this year upon Oxford University Computing Laboratory.'' ---<>--- ``This award goes jointly to Oxford University Computing Laboratory and INMOS Ltd, for the development of formal methods in the specification and design of microprocessors. ``The occam programming language, developed by the applicants has been used to translate the IEEE Standard 754 to cover the floating point arithmetic unit for the IMS T800 floating point transputer. ``The use of formal methods has enabled the development time to be reduced by 12 months.'' ---<>--- For those of you who have never heard of Queen's Awards, I should explain that it is an institutional equivalent of an OBE or a knighthood or something like that. For twenty-five years, awards for Export and for Technological Achievement have been announced on the Queen's birthday (today) which give the recipient the right to display an emblem (`the crown and cogwheels') and generally feel pleased with itself. This is the first time that a department of the University has achieved the distinction of a Queen's Award, and the Computing Laboratory is one of only three university research groups amongst this year's 175 award-winners. The great thing about this award is that it recognises the value of University research in promoting technological development. For those of you who have not heard before of the work being honoured, perhaps I could explain. The award cites the development of occam, which is the first commercially available language to take seriously the problem of programming MIMD parallel machines. Occam goes out of its way to be clear and simple, being designed to be very little more than an implementation of Tony Hoare's CSP. The intellectual leverage gained from the simplicity and elegance of the semantics of occam, is instrumental in the success of the project. The most tangible commercial success is the design of the floating point arithmetic unit in the T800 transputer. The heroes of this tale (the ones who did the work anyway) are Geoff Barrett and David Shepherd, both of whom came to Oxford as students on the MSc in Computation, and both of whom now work for INMOS Ltd in Bristol. At the time the work was done Geoff was in Oxford doing his doctoral research in the Programming Research Group, and David was designing chips for INMOS. When the T800 transputer was designed it was decided that in parallel with an informal development, supported by months of testing against other FPUs, a team would set about a formal development of a correct-by-design unit. In this context `correct' means conforming to the IEEE Standard 754, and a big first step was to decide exactly what the specification required. The IEEE document is partly reliant on the meaning of natural language requirements; Geoff Barrett's recasting of the Standard into the Z specification language [1,2] is unambiguous and serves as the touchstone for the correctness of the T800 FPU. The microcode of the T800 FPU was documented in a restricted subset of occam. Using the occam transformation system developed in Oxford [3], David Shepherd demonstrated that this code was equivalent to a more naturally expressed occam program which had been shown to meet the Z specification. The transformation system builds on the simple semantics of occam, as expressed by Bill Roscoe and Tony Hoare in [4], allowing essentially mechanical proof that two programs -- like the specification of the FPU and the implementing microcode -- have the same effect. You could hardly have made a better case for formal methods, because the race went to the formal development method. Moreover a number of errors were found in the proposed implementation that had not shown up in months of necessarily very limited testing. (Some of the discrepancies found in testing transpired to be mistakes in an implementation by a competitor, against which the simulation of the T800 was being compared.) Not only is it possible to be much more confident in the accuracy of the finished FPU, but this higher quality implementation was cheaper to design, and completed an estimated year ahead of what would otherwise have been achievable. The moral of this tale is that formal methods can not only improve quality, but also the timeliness and cost of producing state-of-the-art products. INMOS, bless them, ought to have made a packet out of getting it right, being confident that they got it right, and doing so on time. The Laboratory has also benefited from the opportunity to develop its work on the underlying theory into something which it has confidence will be useful. There is a very readable non-technical summary of this work in an article in New Scientist last year [5]. The other people in Oxford working on the occam transformation project (of which the T800 FPU work was a part) who implemented the transformation system were Michael Goldsmith and Tony Cox. With Bill Roscoe and others they are involved in a company called Formal Systems, selling just this kind of expertise, which works out of offices in Oxford and in Auburn, Alabama; and Bill is a lecturer at the University of Oxford. References ~~~~~~~~~~ 1. Geoff Barrett, Formal Methods applied to a Floating Point Number System, Programming Research Group technical monograph PRG-58, Oxford University Computing Laboratory, January 1987. 2. Geoff Barrett, Formal Methods applied to a Floating point Number System, in IEEE Trans Soft Eng, May 1988. pp 611-621. 3. Michael Goldsmith, The Oxford occam Transformation system (documentation), Programming Research Group, Oxford University Computing Laboratory, 1988. 4. A. W. Roscoe and C. A. R. Hoare, The Laws of occam Programming, Programming Research Group technical monograph PRG-53, Oxford University Computing Laboratory, February 1986. 5. David Shepherd and Greg Wilson, Making Chips that Work, New Scientist, No 1664, 13 May 1989. pp 61-64. ---<>--- ----------------------------------------------------------------------------- Date: Mon, 30 Apr 90 18:49:21 GMT From: Paul Swatman Subject: Z Meetings I expect to be in England during January and February 1991 (possibly during December 1990 as well) and am interested in attending formal methods/Z tutorials/workshops/user meetings. Will the PRG be offering/hosting any? Are there any other groups (I know about Logica Cambridge and have written to them) which I should contact? - I would like to make the most of my visit. Thanks for your help, Paul Swatman Lecturer School of Computing Science Curtin University of Technology Perth Western Australia ************************** END OF Z FORUM 5.3 ********************************