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!geraint From: Ruaridh Macdonald (on UK.MOD.RSRE) Newsgroups: zforum Subject: Z Forum Issue 2.3 Message-ID: <04 Date: 4 Nov 87 12:29:34 GMT Date-Received: 4 Nov 87 12:31:43 GMT Lines: 179 2nd November 1987 Z FORUM Volume 2 Issue 3 ----------------- ------- ---------------- Today's Topics -------------- Additions to the Z Bibliography More for the Z Bibliography Infix Symbols in Z Please Acknowledge ---------------------------------------------------------------------- Date: Mon, 5 Oct 87 17:58:45 bst From: Dave Neilson Subject: Additions to the Z bibliography Please add the following to the Z bibliography: Dave Neilson Formal Specification Of An Occam Editor M.Sc. Thesis Programming Research Group, Oxford University September 1985 Dave Neilson Z Specification Of A Full Screen Editor Programming Research Group, Oxford University June 1987 Dave Neilson Hierarchical Refinement Of A Z Specification Proc. Foundations of Software Technology & Theoretical Computer Science Pune, India December 1987 ---------------------------------------------------------------------- Date: Tue, 6 Oct 87 09:51:47 bst From: Geoff Barrett Subject: More for the Z bibliography You might like to add: Geoff Barrett Formal Methods applied to a floating-point Number System PRG Technical Monograph 58 ---------------------------------------------------------------------- Date: Mon, 26 Oct 87 10:36:48 GMT From: mike@uk.ac.oxford.prg Subject: Infix Symbols in Z INFIX SYMBOLS in Z -- A Proposal by Mike Spivey This is the first of a short series of articles about various aspects of the design of the Z notation. I have been working recently on a reference manual for Z, and as I wrote down the rules of the notation, I tried to clarify and simplify them where possible. In these articles, I present the results of these efforts as proposals to the wider Z community, in the hope of generating some constructive criticism, or even some agreement. Some of the things I describe will be the same as what you've always understood; some will be different, and deliberately so, for I have sometimes chosen to ignore the more obscure aspects of Z tradition in favour of rules which seem to me clearer or simpler. There may even be some things you've never really understood before, and if there are, then it's all been worthwhile. In future articles, I hope to cover the differences and similarities between ==[X]=========== | | Declaration | Declaration |-------- and |-------- | Predicate | Predicate ---------------- | and the rules for type-checking expressions which contain generic operators. In this article, I plan to explain the rules about infix, prefix and postfix symbols. There are three KINDS of operator symbols: Function Symbols like + Relation Symbols like < Generic Symbols like <-->. In the reference manual, I define infix symbols of all three kinds, prefix generic and relation symbols, and postfix function symbols. These are the ones needed for the standard mathematical library, but obviously others could be added if necessary. There is no need for prefix function symbols, because ordinary identifiers act as functions when they precede an argument. Infix function symbols have a priority from 1 to 6; higher numbers mean tighter binding. Function symbols of equal priority associate to the left: a + b + c = (a + b) + c. Infix generic symbols all have equal priority, lower than any infix function symbols; they associate to the right, so X --> Y --> Z = X --> (Y --> Z). Relation symbols have no priority or association: instead, the predicate a < b < c means (a < b and b < c). A symbol can be named without applying it to arguments: the missing arguments are just replaced by _: so _ + _ is the name of a function which adds numbers, _ < _ is the name of an ordering relation on numbers, and _ <--> _ is the name of a generic constant which gives the space of relations between its parameters. Whenever they occur in an expression, these names must be surrounded by parentheses. These are the meanings of the various kinds of expression: x + y means (_ + _)(x,y) x > y means (x,y) in (_ > _) X --> Y means (_ --> _)[X,Y] disjoint s means s in (disjoint _) F X means (F _)[X] (finite set sign F) R* means (_*) R. The names with _ can be used in declarations as well as expressions: _ + _: Z x Z --> Z _ > _: Z <--> Z There are some standard infix etc. symbols --- there is a table in the manual --- and others may be added as needed, but each symbol must be used consistently throughout a document. There is no notion of a symbol's acting as an infix only in the scope of its declaration, for example. Some specification-processing programs may use a table of symbols which can be extended by the user, but there is no standard way of doing this. Each infix symbol should be introduced to the human reader by explaining its meaning; relative binding powers, where they matter, should be explained by example. There are a few standard symbols which don't fit in with the pattern described so far. The minus sign may be used either as an infix or as a prefix function symbol, giving in effect two symbols (- _) and (_ - _). The notation R (| S |) for the relational image of S through R is an abbreviation for (_ (| _ |))(R,S). Finally, there is the superscript notation for iteration of relations, and a couple of symbols which may be used either as infix function symbols, or as combinators in schema expressions. These rules have been incorporated in a new grammar for Z which will be part of the Z Reference Manual. I am currently working with Steve King to remove any unnecessary differences between this grammar and his; I have relied heavily on his work in producing the manual. The new things in this account seem to be the clear distinction among the three kinds of symbol, and the decision (arbitrary, I admit) to fix on a rather simple set of priorities and associations. Any comments on this proposal will be more than welcome. I am currently polishing the reference manual for publication as a PRG monograph, and I will publish an advertisement in Z Forum when it is available. If you have been, thank you. ---------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Fri, 30 Oct 87 14:34 Subject: Please Acknowledge The routing of electronic mail from this end has recently been changed. Unless you are using an account on the RSRE mail machine, could you please send a message to me (rm%uk.mod.rsre@uk.ac.ucl.cs.nss) to confirm that you have received this copy of the Z Forum. ************************* END OF Z FORUM 2.3 *************************