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!news From: Ruaridh Macdonald (on UK.MOD.RSRE) Newsgroups: zforum Subject: Z Forum Issue 2.1 Message-ID: <28 Date: 28 Jul 87 13:13:58 GMT Date-Received: 28 Jul 87 13:14:58 GMT Lines: 447 28th July 1987 Z FORUM Volume 2 Issue 1 -------------- ------- ---------------- Today's Topics -------------- Z Course at Oxford More for the Z Bibliography Z and Microprocessor Instruction Sets Specification Test A Problem with State Machines Sequences of Schema Operations ---------------------------------------------------------------------- The last issue of volume 1 was number 9. ---------------------------------------------------------------------- Date: Mon, 27 Jul 87 08:55:52 GMT From: Steve King Subject: Z course at Oxford A N N O U N C E M E N T The Programming Research Group, Oxford University, is arranging a course on MATHEMATICS FOR SOFTWARE ENGINEERING Date: 16th - 28th August 1987 Location: Wolfson College Linton Road Oxford OBJECTIVES The primary objective of the two week course is to provide an introduction to the Z notation and the Z approach to software documentation and development. Z is based on mathematics, and a secondary objective of the course is to demonstrate how results from this discipline can be applied to the specification, the design and the reliable construction of computer systems. The development of computer systems of quality is a major challenge, and we will demonstrate how mathematical abstractions, structures, axioms and equations can be used to master the complexity of projects, to improve the documentation and to develop correct code. THE Z NOTATION CONSISTS OF: 1. The Set Theoretical Language, which is similar to a conventional set theoretic notation, but extended with a small number of concepts which allow the 'specifier' to deal easily with concepts, structures and rules which are commonly encountered during the development of software systems. 2. The Schema Language is a simple language for presenting mathematical text within specification/design documentation, and for managing the complexity that arises from the large number of concepts involved in the description of practical systems. THE Z APPROACH CONSISTS OF: 1. Conventions and Style Experience shows that the use of a mathematical notation such as set theory often leads to most unwieldy descriptions when applied to practical systems. The most important part of the Z approach is the conventions and the style which have been adopted for using the Schema Language when presenting descriptions in the Set Theoretic Language. These conventions encourage the separation of concerns and allow for concepts of the system which is being documented to be formally explained in the simplest possible context. This in turn leads to reusable specifications. The conventions are applied to the 'construction' of large documents and use the facilities of the Schema Language to combine existing formalised explanations into explanations of 'compound' concepts, and to update previously formalized explanations. The style in Z documents is a mixture of informal text (e.g. English, pictures) and formal mathematical text. This style enables these documents to be used by other than chief designers (e.g. developers, users, technical writers, managers). 2. A method for analysing the formal parts of a document with the aim to remove contradiction. If a set of requirements is contradictory, a system which meets these requirements cannot be built, and further development of the system should be stopped until the contradictions are removed. 3. A method for formally analysing whether an implementation meets its specification. During development of a system, decisions are made with respect to the representation of Information and with respect to the order of execution of statements in a sequential algorithm. These decisions can be formalised and proved to be consistent with the formally stated requirements. COST 1150 pounds per person. This covers course fees, accommodation and meals. (Including weekend of 22nd and 23rd) REGISTRATION AND ADMINISTRATION Any enquiries should be made to: Emma Sowton (0865) 273849 As there are a limited number of places available (22), please send your registration together with a non-refundable deposit of 200 pounds as soon as possible to: Z COURSE (Wolfson College) Att: Emma Sowton P.R.G. 8-11 Keble Road Oxford OX1 3QD ---------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Tue, 28 Jul 87 11:50 Subject: More for the Z Bibliography %A Steve King %A Ib Holm Sorensen %A Jim Woodcock %T Z: Concrete and Abstract Syntaxes. Version 1.0 %I Programming Research Group, Oxford University %D 21st January 1987 ---------------------------------------------------------------------- Date: Thu, 23 Jul 87 17:12:42 BST From: Jonathan Bowen Subject: Z and microprocessor instruction sets I'd be interested in hearing from anyone who has used Z to specify an instruction set. I have two students at the PRG specifying the Motorola 68000 and INMOS transputer as MSc summer projects at present. I shall also be presenting a spec of the Motorola 6800 which I did as a PRG monograph (details below) at EUROMICRO'87 in Portsmouth this September. MAIN ENTRY: Bowen, J. TITLE: The formal specification of a microprocessor instruction set AUTHOR: by Jonathan Bowen PLACE: Oxford PUBLISHER: Oxford University Computing Laboratory Programming Research GrouD PAGINATION: 72 p. ; 21 cm. SERIES: Technical monograph PRG-60 NOTES: The specification language Z is used to define a micro- NOTES: processor based system in a formal notation. The Motorola NOTES: 6800 8--bit microprocessor is chosen as an example. Its NOTES: simplicity allows the entire instruction set to be covered. NOTES: Memory configuration and interrupts are also included. The NOTES: use of a formal description language allows the possibility NOTES: of verification of the instruction set. Additionally the NOTES: use of Z combined with informal text is sufficiently readable NOTES: for the specification to be used for documentation purposes. ISBN: 0902928422 SUBJECTS: Microprocessors. Motorola M6800. Z specification language. ---------------------------------------------------------------------- From: Gray Girling (Topexpress) Date: Tue, 28 Jul 87 08:31 Subject: Specification Test This is intended to promote discussion about the ability of Z to specify behaviour. The ability of Z to express mathematical statements is undisputed. The language is also used to specify behaviour. The bridge between the ability to make mathematical statements and to specify behaviour is made using a number of conventions (culminating in the concept of an operation schema). It is by no means obvious that this "bridge" reaches far enough - if a language had been devised specifically for the specification of behaviour would it not have more specification-oriented features? Even the concept of "behaviour" is left unmentioned in much of the Z literature. This test is intended to investigate the ability of Z's operation schemas to specify a number of requirements typical of computer systems. The use of operation schemas is an example of a specification convention particularly useful for specifying the behaviour of a function. Other conventions may be necessary. Some usefully specified things for which conventions may be necessary include: . The allowed sequences of operation invocation. . The use of time as an external influence on behaviour. . The way in which one abstraction can be used in the behavioural description of another. . The circumstances in which an operation will take place (e.g. upon a certain event or continuously). . Whether a specification is supposed to be a complete specification or a partial one, covering only specific areas of behaviour. . The specification that an operation should be invoked, as opposed to the use of the specification of that operation's behaviour in specifying the behaviour of something else. The following are the requirements for the test specification. There is a closed system consisting of two kinds of component: (a) a SWITCH which receives messages and turns a lamp either on or off accordingly; and (b) an OPERATOR which emits messages to SWITCHes periodically. You are required to specify a number of things about such a system using Z. This can be done either by providing some Z and a description of why it is thought to provide the required specification or by providing a rationale describing why any such Z is unnecessary. Feel free to introduce additional specification conventions, as long as you can justify their proposed semantics. The questions are: (1) Specify the operation of a SWITCH with particular reference to the functions "on" and "off" which light and put out the lamp. (2) Specify the operation of an OPERATOR, in particular that it is liable to invoke a SWITCH at any time. (3) Specify that neither SWITCHes nor OPERATORs invoke OPERATORs or are invoked by SWITCHes. Try to distinguish invokation from the provision of the same function that is invoked. (4) Specify a system with only three of the above components, two of them SWITCHes and the third an OPERATOR. Specify the system as a whole - do not assume an external element with which interaction is possible. (5) Specify that one of the OPERATORs may not use the SWITCH. (6) Specify an abstraction of two SWITCHes and an OPERATOR called a GROUP in which the SWITCHes are always in different states and which offers a "toggle" operation to a second abstraction called a GROUPUSER consisting of any number of OPERATORs. (7) Specify that a GROUPUSER can only use the "toggle" operation, not the "on" or "off" operations. (8) Specify that the system has no components other than OPERATORs and SWITCHes (but not disallowing abstractions of them such as GROUPs). (9) Specify that nothing other than an OPERATOR can invoke a SWITCH. (10) Specify that there are no operations supported by a SWITCH other than "on" and "off". (11) Specify that OPERATORs are incapable of invoking operations other than "on" or "off". (12) Specify that when an OPERATOR does not issue a command it offers neither an "on" command nor an "off" command. ---------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Mon, 27 Jul 87 14:33 Subject: A Problem with State Machines I have recently been trying to specify properties of operations on state machines in Z and I wondered whether anyone else had run into similar problems to my own, or whether anyone had solutions to offer. I wish to describe a number of state machines which are similar except that they may perform different operations. At the top level of specification I do not want to say what the operations are, but I do want to specify properties of arbitrary sequences of these operations, for example, information flow properties. At a later stage I wish to refine the specifications to give details of what the individual operations do, for a number of different machines. The use of schemas to represent operations is a very attractive one since it neatly packages up together any preconditions, the effects of an operation and any side effects. Also the methods of carrying out refinement using schemas are given in the literature. Thus a promising start would appear to be to define a schema OP as below, with a view to specialising it at a later stage to give details of the state, inputs and outputs. --- OP ---------- | | st, st' : STATE | in? : INPUT | out! : OUTPUT | ------------------ A machine could be defined as a schema which included a set of such OPs, and properties of sequences of members of this set of OPs could be defined. The problems with this approach are: (a) a constraint has to be placed on OP to ensure that the machine is deterministic, i.e. that given st and in? there is only one st' and one out! which can result. (b) The use of selection of schema components starts to get very messy. Given an in? and st we need to pick out the appropriate OP in order to discover st' and out! For example: in the schema for Machine, we have ops : pset OP all op : ops; i? : INPUT; s : STATE cbar op.in? = i? and op.st = s dot op.st' = .... and op.out! = .... Now, instead of schemas we could use functions to represent operations. This automatically overcomes the problem of non-determinism, and results of operations can simply be expressed as op(in?, st). However, the problems arise when we want to do refinement. How do we refine operations expressed as functions into operations expressed as schemas? Or do we have to abandon schemas altogether? Any thoughts on the above matters will be most welcome. ---------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Mon, 27 Jul 87 16:14 Subject: Sequences of Schema Operations When specifying the requirements for certain types of system we need to be able to place restrictions on particular combinations of operations. For example, when specifying a secure document-handling system, we require that in any arbitrary sequence of operations information must not flow from more highly cleared users to less highly cleared users. When reasoning about sequences of consecutive operations on a system, we expect that the state of the system will not change between the completion of one operation and the start of the next. Thus when writing specifications in the Z notation, we are looking for something akin to schema composition, but applied to an arbitrary sequence of operations rather than just to a pair of operations. We suggest the definition of a 'reflexive transitive closure of schemas' by analogy with the reflexive transitive closure of a relation. Let ST be a schema representing the state of some system. Define a general operation OP on the system, such that inputs are taken from a set IN, and outputs taken from a set OUT are generated: [IN, OUT] ___ OP _____________ | | ST; ST' | in? : IN | out! : OUT | -------------------- The operation which results from combining a sequence of OPs will produce a corresponding sequence of outputs. We need to invent names for these sequences, and choose to form them by prefixing a 'sigma' (for 'sequence') to the input and output variable names, giving 'sigma in?' and 'sigma out!'. The 'reflexive transitive closure' is denoted OP* __ OP* ________________ | | ST; ST' | sigma in? : seq INPUT | sigma out! : seq OUTPUT | ----------------------- Thus, given a sequence of n OPs, sigma in? is the sequence formed by taking the in? from each of the n OPs, ST is the same as the ST in the first OP in the sequence. ST' is the final state resulting from carrying out schema composition n-1 times between the n OPs, and sigma out! is the sequence of n out! resulting. Just as schema composition may be applied to more than one input and to more than one output, so may the closure. (A similar effect is achieved if IN and OUT are in fact schemas themselves, or are Cartesian products.) Example ------- Suppose that we are designing a syntax checker for documents written in Z. The document which is input into the syntax checker consists of a sequence of phrases of Z text, and operations are defined which parse each of the different types of phrase. These operations successively build up a data structure, and the only outputs are the reports on the success of the individual parsing operations. The 'state' of the system is the partially-built data structure, which we shall not define here. We simply assert the existence of a set of such data structures, and the empty data structure of that type, 'null'. [DS] null : DS Z documents are built out of Z phrases: [ZPHRASE] doc : seq ZPHRASE Each operation for parsing an individual Z phrase will output a report. [REPORT] __ ParsePhrase _______ | | DS; DS' | phrase? : ZPHRASE | report! : REPORT | ---------------------- The parsing of a sequence of phrases is given by Parse sdef ParsePhrase* The parsing of the complete document is then: Parse[null/DS, doc/sigma phrase?] ************************* END OF Z FORUM 2.1 *************************