From RM@RSRE Mon Mar 24 11:58:09 1986 Via: rlxa ; 24 Mar 1986 11:57:40-WET From: Ruaridh Macdonald (on UK.MOD.RSRE) To: Z Date: Mon, 24 Mar 86 11:55 GMT Subject: Z Forum Vol. 1 Iss. 3 Acknowledge-To: RM@RSRE Message-Id: <24 MAR 1986 11:55:42 RM@RSRE> Status: RO 24th March 1986 Z FORUM Volume 1 Issue 3 --------------- ------- ---------------- Today's Topics -------------- Ascii Representation of Z Texts Word Processing Z FORSITE Rapid Prototyping / Animation Language Specification ---------------------------------------------------------------------- Date: 26 Feb 1986 1301-WET (Wednesday) From: Bernard Sufrin Subject: Word-Processing Z, Ascii representation of Z texts At Oxford we have been using a standard ascii form for Z symbols for quite a while; it arose because we needed to provide a way for our students to type Z on standard ascii terminals. The standard is really quite simple, and can be mechanically processed into a manuscript for almost any "sophisticated" layout language. It also has the advantage that it is fairly readable. For example, the following is the standard definition of the union operator. /[X/] [define] _[u]_: [P] X [x] [P] X [->] [P] X [where] [A] s[1], s[2]:[P]X [.] s[1] [u] s[2] = { x:X [|] x[in]s[1] [or] x[in]s[2] } [end] To explain: / is an escape character which "quotes" anything which follows it, and special symbols are enclosed in [...]. Our processor is clever about [define] (and [schema]), and inserts instructions to the post-processor which build the left-hand edge of the box. A cleverer processor would measure the width of the material inside the box and adjust the length of the top and bottom bars accordingly. The notation was designed before we changed over from <...> for sequences to [...], and so would probably be a bit irritating now. I propose instead to use // to stand for / (we rarely use /), and to enclose special symbols in /../. The previous definition would become: [X] /define/ _/u/_: /P/ X /x/ /P/ X /->/ /P/ X /where/ /A/ s/1/, s/2/:/P/X /./ s/1/ /u/ s/2/ = { x:X /|/ x/in/s/1/ /or/ x/in/s/2/ } /end/ I suggest the following manuscript notation: /define/ introduces a double (definition) bar /schema,foo/ introduces a single (top of schema) bar, with "foo" embedded /where/ is the short single bar separating signature from axiom /axiom/ ditto /end/ is the long end-definition bar /1/ /2/ ... subscript digits /u/ union /n/ intersection /o/ composition /+/ overriding ^ append sequences /<|/ domain restrict /|>/ range restrict /<~|/ complement domain restriction /|~>/ /|\/ sequence range restriction /\|/ sequence domain restriction /|/ vertical bar in a comprehension /./ fat dot in a comprehension /|->/ maps-to /F/ finite subsets /P/ powerset /x/ product set /defs/ defines syntactically (^ on =) /((/ proper subset /((=/ subset /))/ etc. /<->/ relation /+>/ partial function /->/ total function /++>/ finite mapping />->/ etc. ad nauseam /A/ for all /E/ exists /E1/ unique existence /=>/ implication /<=>/ iff /<=/ /or/ /and/ /geq/ /leq/ />/ / Date: Mon, 3 Mar 86 13:34 Subject: Word Processing Z At RACAL ITD we have produced a symbol set for Z and CSP using the font tool on SUN workstations. This symbol set is loaded into a redifinable font on our QMS LASERGRAFIX printer using a C procedure. We are currently able to access approximately 110 of the 128 character positions available in this font (due to troff limitations). This symbol set is loaded onto the printer whenever a request is made to print a Z / CSP document. Our documents are stored under UNIX in a pair of sibling directories. One of these contains information that does not appear in the schemata of the document, together with references to the schemata which are stored in the sibling directory. Printing of the document initiates the following up of these references and the insertion of the schemata into the appropriate in the document. Plans are underway for the integration of Oxford's WYSIWYG editor (QED) with a formal language checker and a proof system, this will run on SUN equipment. - - - - - N.B. WYSIWYG = What You See Is What You Get. Editor. ---------------------------------------------------------------------- From: PAUL A BURCH (on ALVEY at Teddington) Date: Thu, 6 Mar 86 11:56 Subject: FORSITE RACAL ITD are working on an Alvey project called FORSITE. Our collaborators on the project are Systems Designers, Oxford University and Surrey University. The aim of FORSITE is to provide a toolset for the production and maintenance of Z or CSP specifications. By August we will have implemented the first stage of FORSITE, which will include an editor, a formal language checker and a proof system. The editor will be WYSIWYG with multi font capability. The formal language checker will parse expressions in Z or CSP, and provide type checking facilities for Z. The proof system will aid an user in the proof of theorems. The idea of various interrogative tools is also being considered, for example, expanding schemas down to base level declarations. We would welcome suggestions for tools that readers of this forum feel would be of particular use in the production of Z or CSP specifications. ---------------------------------------------------------------------- From: DAVID R F BOSOMWORTH (on ALVEY at Teddington) Date: Mon, 3 Mar 86 14:35 Subject: reply to rapidprototyping /an{mation Here are a number of points to bear in mind when considering the question of rapid prototypes for formal specs : 1. Rapid prototyping seems to fit nicely into the iterative process of specification writing, allowing the customer to disagree, and generally highlighting areas of contention ... BUT 2. When we produce a formal specification, we are probably trying to develop a "theory" about the system that we are tring to model. We probably want to trya and derive some "general results" about our model. 3. Rapid prototyping only permits "pointwise" testing of our problem domain. This seems to imply that rapid prototyping can only be used to show "inconsistencies", and not "consistencies". 4. We have the problem of : "does the rapid prototype actually prototype our specification ?" 5. We have to consider the effort needed to generate a rapid prototype against the benefits that may be gained. The "formal" benefits are negligible, because the rapid prototyping process does not remove the proof obligation that is placed upon the author. {In short rapid prototypes are great for getting more money out of managers, and highlighting "incorrect" specs, but no good for showing the correctness of specs. The above are my own views - hope they spark off some argument David Bosomworth. ---------------------------------------------------------------------- From: Colin O'Halloran (on UK.MOD.RSRE) Date: Fri, 21 Mar 86 09:18 GMT Subject: Z-Forum To the Z-Forum: Has anybody any examples of Z being used to specify a language. Has anybody got examples of using the typed lambda abstraction beyond the examples given in case studies and is the semantics of the lambda abstraction available? Thanks Colin O'Halloran. **************************** END OF Z FORUM **************************