From RM@RSRE Tue Oct 28 12:08:57 1986 Via: rlxa ; 28 Oct 1986 12:08:54-WET From: Ruaridh Macdonald (on UK.MOD.RSRE) To: Z Date: Tue, 28 Oct 86 12:00 Subject: Z Forum Issue 9 Acknowledge-To: RM@RSRE Message-Id: <28 OCT 1986 12:00:58 RM@RSRE> 28th October 1986 Z FORUM Volume 1 Issue 9 ----------------- ------- ---------------- Today's Topics -------------- More for the Z Bibliography Bibliography - Case Studies Binding of Logical Connectives Syntax Rules of Inference ---------------------------------------------------------------------- Date: Wed, 30 Jul 86 15:36:58 GMT From: sufrin@ruskin (Bernard Sufrin) Subject: More for the Z bibliography %A Bernard Sufrin %T Formal Methods and the Design of Effective User Interfaces %B People and Computers: Designing for Usability %E M.D. Harrison, and A.F Monk %I Cambridge University Press %D 1986 %A Christopher Kalus %T Applicative Languages for Data Processing %R D. Phil. Thesis %I Oxford %D 1980 %A Bernard Sufrin %T Formal Specification: notation and examples %B Tools and Notations for Program Construction %E D. Neel %I Cambridge University Press %D 1982 %X Example of a filing system specification, first published use of the schema notation to put together states. %A Bernard Sufrin %T Specification and Development of a Reliable Filestore %R PRG working paper %D 1983, 1984 ---------------------------------------------------------------------- Date: Fri, 24 Oct 86 09:58:56 GMT From: Jonathan Bowen Subject: Bibliography - Case Studies Here are the details of the new Z book: %A Bill Flinn %A Roger Gimson %A Ian Hayes %A Carroll Morgan %A Ib Holm Sorensen %A Bernard Sufrin %T Specification Case Studies %S Prentice-Hall International Series in Computer Science %E Ian Hayes %I Prentice-Hall International %P 332 %D 1986 %K Z Language, Formal Specification %L ISBN 0-13-826579-8, ISBN 0-13-826595-X PBK Paperback and hardback versions both available now. Pbk c 15 pounds, Hrdbk c twice as much off the top of my head. There is much work going on in the area of Z standardisation and tools so I hope you get some more responses. ---------------------------------------------------------------------- From: Trevor E G King (on UK.MOD.RSRE) Date: Fri, 24 Oct 86 11:49 Subject: Binding of Logical Connectives In section 2.6.1 ("Logical expressions") of "A Syntax for the Z Notation", Draft 2.1, Aug 28, 1986, produced by PRG, it's stated that V, => and <=> possess the same binding power, with any ambiguity resolved by appealing to the left-associativity of these connectives. This is in contrast to the commonly accepted convention (the adjective may be tautological!) that V, => and <=> have decreasing binding power. Thus both conventions interpret P1 V P2 => P3 as (P1 V P2) => P3, but P1 => P2 V P3 is interpreted in the conventional way as P1 => (P2 V P3), whilst in Z it would appear to be (P1 => P2) V P3. I find the conventional interpretation less confusing. Was there a good reason for the change?? ---------------------------------------------------------------------- Date: Tue, 28 Oct 86 10:17:41 GMT From: Steve King Subject: Syntax News of syntaxes: Latest (final?) version of `A Syntax for the Z Notation' (King, Woodcock, Sorensen) should appear by Nov 26---the date of our project review meeting. This will supercede previous versions of both concrete and abstract syntaxes, since this document will have everything in it! Could you update the bibliography accordingly ---------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Tue, 28 Oct 86 11:32 Subject: Rules of Inference Have any case studies been published which show the use of the rules of inference published in the draft Z Handbook, especially their use in proving theorems related to Z Specifications? *************************** END OF Z FORUM 1.9 ***********************