From RM@RSRE Mon Feb 24 15:32:29 1986 Via: rlxa ; 24 Feb 1986 15:32:19-WET From: Ruaridh Macdonald (on UK.MOD.RSRE) To: Z Date: Mon, 24 Feb 86 15:31 GMT Subject: Z Forum, Volume 1 Issue 2 Acknowledge-To: RM@RSRE Message-Id: <24 FEB 1986 15:31:45 RM@RSRE> Status: RO 24th February 1986 Z FORUM Volume 1 Issue 2 ------------------ ------- ---------------- Today' Topics ------------- Re. Type Checking of Z by Machine Reader Replies to Z Forum Issue 1 Z Handbook Sending Z Texts Over Mail Rapid Prototyping / Animation Word Processing Z -------------------------------------------------------------------------- From: CMOH@RSRE (on UK.MOD.RSRE) Date: Mon, 24 Feb 86 10:08 GMT Subject: Re. Type Checking of Z by Machine Reader Dear Ruaridh, In reply to Q2 of your Z forum message I think that the Edinburgh ML approach should be taken. To recap we have a : A; c: C; f :A -> B; g :B -> C; h :(A -> B) -> (C -> D); Now if we insist that a Z reader imposed strong type checking as in ML then the reader would be able to deduce that gfa means g(fa) since this would be the only way to parse the expression and obey the type checking. Similarly hfc could only be parsed as (hf)c. If the reader were used like the Edinburgh ML interpreter the type of each expression could also be displayed after it had been defined or used, this would make it clear to the user exactly what the type of the expression in hand was, which would be useful if he/she was entering some complicated expression. This of course would mean that brackets would not be needed for such expressions as hfc. This might be an objection to using the type checking to parse expressions, however I believe that clarity of Z expressions ought to be left to the user and not rigidly imposed by a Z reader. ------------------------------------------------------------------------- Date: Fri, 21 Feb 86 14:13:23 GMT From: Mike Spivey Subject: Replies to Z Forum Issue 1 CONTRIBUTION TO Z FORUM. Mike Spivey, 21/2/86. I'm trying to keep the following short, so I apologize in advance if it's too short to make sense. The views expressed are (of course) mine alone. Q1. Do we need new constructs ... to specify algorithms adequately [in program development]? A. We work with the idea of using programming-language constructs to combine pieces of specification. One way of looking at this is to say that programs are just low-level specifications which happen to contain only constructs executable on our computer, and to look on semicolon, WHILE-DO, and so on, as operations which combine specifications, whether they have the form of a program or not. `Monotonicity' properties of the common programming constructs ensure that e.g. if R0 refines S0 and R1 refines S1 then (R0; R1) refines (S0; S1) - this allows for `stepwise refinement'. Another way of looking at this is to have a special fictitious command `SPEC S' in the programming language; this behaves as if it satisfied the specification S, although it isn't really implemented by the computer. Program development proceeds by replacing SPEC statements step-by-step with program fragments which implement them. This approach seems to work quite well with program fragments specified by `homogeneous' schemas - those of the form [STATE; STATE' | ... ]. I don't know of any substantial examples which have been done formally in this way, although all the ingredients are well-known. It would be interesting to try mixing this style with the `schema-calculus' style of specification. Q2. [Should we use type-checking to disambiguate the term g f a, which could be read as g (f a) or (g f) a ?] A. [Dogmatic (though correct) opinion]: 1. DON'T USE SEMANTICS TO DISAMBIGUATE SYNTAX! a. Because it makes things more difficult for the human reader. b. Because type-errors may cause the (human) writer and the (machine) reader both to succeed with parsing, but in different ways. c. Because it makes it impossible to generate intelligible error messages. d. Because it complicates the task of writing the parser, and so diverts resources from more important activities. 2. Make --> right-associative: A --> B --> C = A --> (B --> C), and application left-associative: f a b = (f a) b. These simple conventions fit well together - in the example above, the types are f: A --> B --> C; a: A; b: B - and in practice works better than the opposite conventions. If f: B --> C; g: A --> B; a: A, you have to use brackets in f (g a), but many people are happy to write f(g(a)) anyway. Q3a. Should we [try] to make ... proof ... simple ... ? A. Of course! Q3b. Is it possible? A. I hope so! Q3c. How? A. Well, there seems to be some expectation that MECHANIZED ASSISTANCE will be of use in organizing and checking proofs. Two good reasons for this expectation are: 1. Formal methods give rise to mathematical texts which are LENGTHY; so some help with organizing and presenting the text will be of use. 2. The mathematics in such texts is rather SHALLOW, so we might hope that the formula-manipulation in proofs could be mechanized. I don't however place much faith in fully-automatic theorem provers. This not because of their weakness in proving true results, but because of the situation when they fail to prove a FALSE one. The programmer then needs to find his mistake and correct it, and the remains of a failed proof-attempt often give little help with this. Also, if small changes to the specification are made, the way to find the corresponding (small, we hope) changes to the implementation is by analysis of the refinement proofs. For these reasons, I don't feel that the composition of proofs is a task which the programmer can afford to delegate wholly to a machine. ------------------------------------------------------------------------ Date: 21 Feb 1986 1629-WET (Friday) From: Bernard Sufrin Subject: Z Handbook Ruaridh: Work is in progress and should finish by mid-March on a full Z handbook. This will include the original Notes for a ... together with materials on the schema calculus, the type system, and the proof system. B. -------------------------------------------------------------------------- Date: Fri, 21 Feb 86 11:27:40 GMT From: Jonathan Bowen Subject: Sending Z Texts Over Mail How about a proposal for a standard ASCII version of Z so that specs can be transmitted by electronic mail etc easily - eg for the Z Forum! Perhaps you could suggest this in the next newsletter. I haven't though about it too much yet but basically you would just need a list of corresponding ASCII strings for each of the "standard" Z symbols. I would be willing to come up with a suggested list when I have the time. Jonathan --------------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Mon, 24 Feb 86 10:16 GMT Subject: Rapid Prototyping / Animation When we develop a system by writing out a specification for it (perhaps in Z) and producing an implementation based on that, we probably want to have some confidence that the specification accurately reflects what we had in mind. We do not want to find that the effort expended on producing the implementation has been wasted because the system was incorrectly specified. Should we be able to try out the specification in some way by being able to execute it with test data, by 'rapid prototyping' or 'animation', or can the specification be developed in such a way as to make this unnecessary? -------------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Mon, 24 Feb 86 11:09 GMT Subject: Word Processing Z At RSRE, we have produced a symbol set for Z, for use on the VT200 range of terminals working in 8 bit mode. We are hoping to be able to drive a DEC laser printer (LN03) using the same symbol set once we have worked out how to format the file for loading characters into the printer. (Neither of the pieces of software are of production quality, as they have only been developed quickly for our own use.) We have a VAX system, using the VMS operating system. This system has the advantage that it will be able to support the development of software for mechanised assistance with Z at a later date, but there is space for only 80 new characters (soon filled up by Z!) The VAX is also in widespread use, so that software (particularly that involving unusual characters) can be shared among a number of users. We may also use an Amstrad for word processing Z, since it allows more user-defined characters. However, it would not have the ability to support mechanised assistance for Z. What are other people doing for word processing Z? *************************** END OF Z FORUM *****************************