From RM@RSRE Wed Apr 30 16:23:47 1986 Via: rlxa ; 30 Apr 1986 16:22:57-WET From: Ruaridh Macdonald (on UK.MOD.RSRE) To: Z Date: Wed, 30 Apr 86 17:22 GMT Subject: Z Forum Issue 5 Acknowledge-To: RM@RSRE Message-Id: <30 APR 1986 17:22:04 RM@RSRE> Status: RO 30th April 1986 Z FORUM Volume 1 Issue 5 --------------- ------- ---------------- Today's Topics -------------- Rapid Prototyping, ASCII Transmission of Z uP Instruction Set Specification in Z Reports and Publications Parsing, Recursive Fuctions, etc. Specification of Timing Constraints ---------------------------------------------------------------------- Date: Mon, 21 Apr 86 10:46:14 est Subject: Rapid Prototyping, ASCII Transmission of Z From: sufrin Interest in Z is burgeoning in Australia. There's the beginnings of a Z tools group at the University of Queensland, who are adapting the Rose/Welsh method of building syntax-oriented editors to work with a standard form of Z. Apropos "rapid prototyping": there have been some experiments here in "running" Z, by coding definitions as prolog rules. The result is S L O W (continental drift) but if you have the patience, you get the gratification of seeing the system take 25 minutes to do an empirical validation of one case of a theorem which you could have proven in 5 minutes! I suppose it all depends what expectations are raised by the "rapid" in "rapid prototyping" . Apropos standards for Ascii transmission of Z material: my contribution was just a suggestion -- the System Designers way is just as acceptable -- indeed probably more so since they already have vast amounts of material in that form. - - - - - N.B. A list of the ASCII symbols to be used in place of the usual Z symbols will appear in the next version of the document defining the concrete syntax of Z. Editor. ---------------------------------------------------------------------- Date: Fri, 25 Apr 86 10:51:09 GMT From: Jonathan Bowen Subject: uP Instruction Set spec in Z I have recently specified the instruction set of a simple 8-bit microprocessor (the Motorola 6800) in Z. The spec worked out suprisingly well, and Z would be very suitable for use in an instruction set manual. Is anyone else interested in specifying instruction sets, and has anybody else attempted this in Z? If so, I would like to hear from them. I can send a copy of the paper, and would be interested in any comments on it. -- Jonathan Bowen, Programming Research Group. Tel 0865-54141, Mail: bowen@uk.ac.ox.prgv (JANET), ...!ukc!ox-prg!bowen (UUCP) ---------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Fri, 25 Apr 86 12:02 GMT Subject: Reports and Publications At a meeting of developers of Z and tools for Z, I agreed to compile a list of publications (papers, reports, etc.) which relate to Z and its associated techniques, and which are available to users of Z and other interested parties. Some examples of the topics which would be of interest are descriptions of Z, case studies, techniques of specification, refinement and implementation, mathematical foundations, comparisons with other methods, and critiques. This list is by no means complete, and if you feel that you have something relevant to offer, please let me know. The details I need are (modified as appropriate): 1. Title 2. Author(s) 3. Publisher 4. Date and Version Number 5. Book or journal in which paper appears 6. How to get copies (Name and Address of Author / Library / etc.) 7. Any previous publications which are included in or superceded by this one. 8. Any later publications which include or supercede this one. I will publish these details in the Z Forum, as well as making them more widely available. Please send details either by electronic mail to RM@RSRE, by snail mail to Ruaridh Macdonald, Room Q212, R.S.R.E., St. Andrews Road, Malvern, Worcestershire. WR14 3PS or 'phone me on Malvern (06845) 2733 Ext 3846. ---------------------------------------------------------------------- From: Colin O'Halloran (on UK.MOD.RSRE) Date: Wed, 30 Apr 86 15:34 GMT Subject: Parsing, Recursive Functions, etc. Does anyone have any examples of Z specifications which specify operations on recursively defined objects, perhaps a specification of a parser? As a simple example, how would you specify the operation of evaluating arithmetic expressions such as 2+4-(5-(6+2)-(4-3)), with the following syntax: term ::= (expr) | number expr ::= expr + term | expr - term | term ? (Thus, given the expression above, I want a specification of the function which will yield the result 10.) ---------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) To: RM Date: Wed, 30 Apr 86 15:51 GMT Subject: Specification of Timing Constraints Message-Id: I have not yet seen any examples of Z being used to specify timing constraints on a specification. The sort of thing I have in mind is: 1. This operation must be completed within 10ms. 2. The total time taken to carry out this sequence of operations must be less than 40 ms. 3. Spend 50ms carrying out this operation, then exit, regardless of whether the operation is complete. Is it ridiculous to suggest trying to incorporate timing constraints into a Z specification? Would it be better to express timing constraints some other way? If it can be done with Z, how? And what rules of refinement are applicable? Ruaridh *************************** END OF Z FORUM ***************************