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 (on UK.MOD.RSRE) Newsgroups: zforum Subject: Z Forum Issue 3.3 Message-ID: <24 Date: 24 Jun 88 10:01:09 GMT Date-Received: 24 Jun 88 10:02:03 GMT Lines: 223 24th June 1988 Z FORUM Volume 3 Issue 3 -------------- ------- ---------------- Today's Topics -------------- Z Course at Oxford Z Typechecking Environment Condense (Brainteaser) --------------------------------------------------------------------- Date: Mon, 20 Jun 87 08:55:52 GMT From: Jim Woodcock 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 Z - MATHEMATICS FOR SOFTWARE ENGINEERING Date: Sunday 14th - Friday 26th August 1988 Location: St. Edmund Hall Queen's Lane Oxford OX1 4AR 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 Course tuition fees are #1300.00 per person. Accommodation costs are separate, amounting to #270.00 for the two week course, NOT staying over the middle weekend, or #305.00 for the two week course, including the middle weekend. Wines, etc., to be paid for separately. Over the middle weekend, only bed and breakfast is available, not full board. On Thursday 25th August, there will be a conference dinner, for which there is an extra charge of #5. VAT is not chargeable on these fees under present regulations. REGISTRATION AND ADMINISTRATION Any enquiries should be made to: Industrial Liaison Secretary (0865) 272568 As there are a limited number of places available (16), please send your registration together with a non-refundable deposit of 300 pounds as soon as possible (not later than 31st July) to: The Industrial Liaison Secretary P.R.G. 8-11 Keble Road Oxford OX1 3QD ---------------------------------------------------------------------- From: sufrin@uk.ac.oxford.prg Date: Thu Jun 16 17:27:55 1988 Subject: Z Typechecking Environment Z Typechecking Environment I am about to release a typechecking environment for Z. It is considerably faster than the Forsite prototype, to which it is unrelated except by purpose. It can work either with annotated QED files or in ascii (those addiXted to TeX or any other formatting tool can also be accomodated). The tool can be used incrementally or in "batch" mode, and supports the saving of predefined "theories" for later use. Type error messages are fairly helpful, the type of every item defined is published, and a simple interactive schema calculation facility is also provided. Almost nothing is built in to the environment (for example it doesn't even start off knowing the syntax or meaning of function arrows). Users are therefore free to define their own Z libraries from scratch, including all or none of the "standard" library as they see fit. The environment provides for user definition of any number of infix, (_?_), prefix (?_), postfix (_?), leftfix (_??_??), rightfix (??_??_), outfix (??_??) and midfix (_??_??_) operators. In the QED version super- scripting and subscripting can be assigned special meaning if this is deemed necessary in a particular problem-oriented notation. I believe that it supports "Z as she is published", except for the "offside rule for quantifier scoping, and for the fact that the binding power and syntactic associativity of infix operators must be explicitly declared. Overloading of symbols under user control is also supported (it isn't neces- sary to have different symbols for subtraction and set-difference, for example, or for real, integer, and natural arithmetic operations). Further particulars are available, and I am happy to give demonstrations of the tool (either in Oxford or Hawaii) given reasonable notice. Bernard Sufrin, Programming Research Group Oxford. --------------------------------------------------------------------- From: Alfred.Smith (on UK.MOD.RSRE) Date: Tue, 14 Jun 88 11:06 Subject: Condense (brainteaser) In reply to the brainteaser (Z forum - 20 Jan 1988) I propose the following solution: Define the condense function c, and the partial condensation function pc, as follows [X] |================================================================== | c : seq1 X --> seq1 X | pc : seq1 X --> |P seq1 X |------------------------------------------------------------------ | For All s : seq1 X ; x : X . | c() = | pc() = { } | last s = x ==> c(s^) = c(s) | pc(s^) = { u:pc(s) . u^ } U pc(s) | last s /= x ==> c(s^) = c(s) ^ | pc(s^) = { u:pc(s) . u^ } |------------------------------------------------------------------ These definitions, of course, lend themselves to proof by induction. By proving the lemma For All s : seq1 X . For All u : pc(s) . last u = last s the theorem For All s : seq1 X . For All u : pc(s) . c(u) = c(s) can then be proved. As both the lemma and the theorem are of the form For All s : seq1 X . P(s) then each can be proved in the 2 steps For All x : X . P() For All s : seq1 X ; x : X . P(s) ==> P(s^) with the latter induction step being split into the 2 cases last s = x and last s /= x because of the definition. ************************* END OF Z FORUM 3.3 ************************