Relay-Version: version B 2.10.2 9/18/84 +2.11; site UK.AC.OX.PRGV Posting-Version: version B 2.10.2 9/18/84 +2.11; site UK.AC.OX.PRGV Path: OX.PRGV!news From: Ruaridh Macdonald (on UK.MOD.RSRE) Newsgroups: zforum Subject: Z Forum Issue 6 Message-ID: <786@UK.AC.OX.PRGV> Date: 11 Jun 86 13:26:23 GMT Date-Received: 11 Jun 86 13:26:23 GMT Sender: news@UK.AC.OX.PRGV Organization: PRG, Oxford University, UK Lines: 626 3rd June 1986 Z FORUM Volume 1 Issue 6 ------------- ------- ---------------- Today's Topics -------------- Parsing, Recursive Functions, etc. Evaluating Expressions in Z Specification of Timing Constraints Decoration of Schemas, and Subscripting Z and Auto-G Miscellaneous Queries Word Processing Z Reminder of Bibliography Mailing List ---------------------------------------------------------------------- From: Anthony Hall Date: Fri, 9 May 86 16:26:33 bst Subject: Parsing, Recursive Functions, etc. (Re. Z Forum Issue 5) Yes indeed, Aspect is doing something very like that. We haven't finished the work yet, but an example of what we are doing is as follows: Consider the view mechanism in a database. This defines some objects in terms of expressions over other, lower level objects. For example a = b+c Now we want a hierarchy of views, so that b and c are themselves view objects b = d-e c = f*g Eventually one arrives at objects which are not view objects, but really exist in the database. Now what we want to do is "compile" any view expression into an expression in terms only of these base objects. For example a = d-e + f*g The technique we are using for this and similar problems is to model expressions in terms of directed graphs. We did consider defining expressions in terms of recursive disjoint union, but didn't get very far because we couldn't see how to manipulate them in that form. Furthermore we have already developed a generic "theory of digraphs" in Z for general use within Aspect, so we could draw on that. (Which raises another issue. Is it likely that such a theory is likely to be useful to others - do we want a specification library on Z forum?) I hope the specification of this "compilation" will be available quite soon. We have also looked briefly at the evaluation of an expression which looks, actually, much more straightforward to express. Most of this is being done by Alan Brown at the University of Newcastle. ------------------------------------------------------------------------ From: Jonathan Bowen Date: Fri, 30 May 86 14:59 GMT Subject: Evaluating Expressions in Z The following is in response to a question in the last Z Forum. Consider a function to evaluate expressions defined by the following BNF syntax: digit ::= '0'|'1'|'2'|'3'|'4'|'5'|'6'|'7'|'8'|'9' number ::= digit {digit} term ::= '('expr')' | number expr ::= expr '+' term | expr '-' term | term The basic set of symbols may be broken down into digits, brackets and operators: DIGIT = {'0','1','2','3','4','5','6','7','8','9'} BRACKET = {'(',')'} OP = {'-','+'} SYMBOL = DIGIT U BRACKET U OP A non-empty sequence of digits can be evaluated to a natural number: | | number : seq DIGIT -+> $N$ |__________________________________________________ | | number ['0'] = 0 | number ['1'] = 1 | number ['2'] = 2 | number ['3'] = 3 | number ['4'] = 4 | number ['5'] = 5 | number ['6'] = 6 | number ['7'] = 7 | number ['8'] = 8 | number ['9'] = 9 | | | $forall$ s : seq DIGIT | #s>1. | number(s) = 10 x number(front s) + number(last s) Terms and expressions, consisting of a sequence of symbols, can be evaluated to an integer value as follows ($cat$ represents concatenation of sequences): | | term, expr : seq SYMBOL -+> $Z$ |_________________________________________________ | | $forall$ s : dom expr; n : dom number. | term(['('] $cat$ s $cat$ [')']) = expr(s) $and$ | term(n) = number(n) | | $forall$ s : dom expr; t : dom term. | expr(s $cat$ ['+'] $cat$ t) = expr(s) + term(t) $and$ | expr(s $cat$ ['-'] $cat$ t) = expr(s) - term(t) $and$ | expr(t) = term(t) Note that the domain of numbers is contained within the domain of terms, which in turn is contained within the domain of expressions: $theorem$ dom number $subset$ dom term $subset$ dom expr (These sets are the smallest which satisfy the above functions.) ------------------------------------------------------------------------ From: Jonathan Bowen Date: Fri, 30 May 86 15:30 GMT Subject: Specification of Timing Constraints This note is in reply to a question in the last Z Forum. We shall consider absolute time and time intervals (the difference between two absolute times). [ Time, Interval ] We take it for granted that time is totally ordered: | | _$leq$_ : Time <-> Time |_____________________________________________ | | _$leq$_ $elem$ total_order Time | The concept of the current time may be included in the system state: _ SYS _______________________________________ | | : | now : Time |_______________________________ | | : |____________________________________________ Now consider changes in state to the system during an operation. We include the time period taken to execute the operation explicitly, for convenience: _ $delta$SYS ________________________________ | | SYS | SYS' | period : Interval |________________________________ | | now $leq$ now' | period = now' - now |____________________________________________ Suppose we wish to limit the time an operation can take to execute. We can simply add a predicate to this effect to the specification of the operation: MaxTime : Interval _ OP ________________________________________ | | $delta$SYS | : |________________________________ | | period $leq$ MaxTime | : |____________________________________________ This can easily be extended to a series of operations: OP $sub$AB = (OP $sub$A ; OP $sub$B) | period $leq$ MaxTime Consider the case where we wish an operation to time out if it cannot be performed within a certain time period. We assume that the system state (apart from the current time) does not change if a time-out occurs in this example: _ OP ________________________________________ | | $delta$SYS | : | report! : Report |_______________________________ | | period < MaxTime ==> | ( : | report! = Success) | | | period = MaxTime ==> | ( SYS' $hide$ now' = SYS $hide$ now $and$ | report! = TimeOut) |___________________________________________ ------------------------------------------------------------------------ From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Fri, 30 May 86 15:35 GMT Subject: Specification of Timing Constraints One further definition is required in the above: | | _-_ : Time $x$ Time -> Interval |____________________________________________ | | : | ------------------------------------------------------------------------ From: Jeff Sanders Date: Fri, 30 May 86 16:56 GMT Subject: Specification of Timing Constraints 0. Suppose operation AOP on states AS is specified: _ AS _______________________________________ | | a : . . . |___________________________________________ _ AOP ______________________________________ | | $delta$ AS | in?, out? : . . . |___________________________________________ | | P(a, in?, out?, a') |___________________________________________ Introduce time into the state by setting _ AS $sub$ t _______________________________ | | AS | t : (0, $inf$) |___________________________________________ where $inf$ represents infinite time. We think of AS $sub$ t as representing the time at which AS occurred. The operation is augmented, for instance: _ AOP ______________________________________ | | $delta$ AS $sub$ t | in?, out? : . . . |___________________________________________ | | P(a, in?, out?, a') | t < t' < t + 10ms |___________________________________________ In other words the duration of AOP is at most 10ms. 1. Note. There is an alternative way to introduce duration into an operation, which seems more complicated when we come to refinement. It consists of augmenting the original AOP as follows: _ AOP ______________________________________ | | $delta$ AS ; I/O ; | d : AS $x$ I $x$ O $x$ AS' -> (0,$inf$) |___________________________________________ | | P(a, in?, out?, a') | d(a, in?, out?, a') < 10ms |___________________________________________ where d represents duration. 2. Suppose operation COP on states CS is _ COP ______________________________________ | | $delta$ CS $sub$ t |___________________________________________ | | Q(c, in?, out?, c') |___________________________________________ Then COP refines AOP iff for each applications program P, P $sub$ COP $subset$ P $sub$ AOP. (This is the usual definition of refinement; applications programs are written in a language like Dijkstra's language of guarded commands.) As usual, this definition is difficult to verify and the usual relational sufficient conditions are used. 3. Specification for sequential composition is like "convolution": suppose that for 1 $leq$ j $leq$ n _ AOP $sub$ j ______________________________ | | $delta$ AS $sub$ t | I/O |___________________________________________ | | P(a, in?, out?, a') | t < t' < t + e $sub$ j |___________________________________________ Then we require AOP $sub$ 1 ; . . . ; AOP $sub$ n to satisfy $sigma j=1 to n$ e $sub$ j < 40ms, for example. 4. Timeout is like error handling, of course. _ AOP' _____________________________________ | | $delta$ AS $sub$ t | I/O |___________________________________________ | | P $and$ (t < t' < t + 50ms) | $or$ | (t' $geq$ t + 50ms) $and$ EXIT |___________________________________________ where EXIT can be determined by a schema. ---------------------------------------------------------------------- From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Mon, 19 May 86 15:47 GMT Subject: Decoration of Schemas, and Subscripting We wish to consider the inputs and outputs belonging to each user of a computer system completely separately from the inputs and outputs of the other users. As a result we end up talking about a set of abstract machines, each one corresponding to the view one user has of the whole system. We therefore wish to define a schema which represents one abstract machine, and decorate it to represent different members of the set of abstract machines. [States, Inputs, Outputs] $schema, Machine$ S : $P$ States I : $P$ Inputs O : $P$ Outputs . . . $where$ . . . $end$ This represents the general abstract machine. I now wish to refer to individual machines, using Machine$sub$c where c:C, C being some set simply declared using [C]. I assume this is permissible and well defined in Z. A further problem arises in trying to relate the abstract machines to the overall machine. The state of the overall machine is the cartesian product of the states of the abstract machines. Thus if C = 1..n for some natural number n, StateSet $defeq$ State$sub$1 $X$ State$sub$2 $X$ .. $X$ State$sub$n (I don't know if $defeq$ is standard for 'defined equal to' - I'm guessing!) This could also be written: StateSet $defeq$ $XX1..n$ State$c$ where $XX1..n$ is intended to represent a large cartesian product symbol with 'c = 1 to n' around it. The problem arises when C is a set without a natural total ordering on it - the order of the cartesian product is ambiguous. Any thoughts on this issue? ------------------------------------------------------------------------ Date: Tue, 20 May 86 13:03:14 GMT From: Mike Spivey Subject: Decoration of Schemas, and Subscripting You seem to be trying to get more value out of decoration than is really there: in particular, I can't really see a way to make sense of variables which "range over decorations", and you seem to be working in that direction. You might consider modelling the state of the whole machine as a function from machine-id's (your set C, I think) to abstract machine states. Roughly, ABSM___ | | -- the abstract machine's state variables | |--- | | -- whatever | ------- STATE___ | | state: C --> ABSM | -------- Now you can describe operations on a single abstract machine by schemas in the shape of deltaABSM: DeleteFile___ | | ABSM | ABSM' | fn?: NAME | |--- | | -- and so on | ------------- These operations can be 'promoted' to the whole state by using the 'framing' schema phiABSM___ | | ABSM | ABSM' | c: C | STATE | STATE' | |--- | | thetaABSM = state(c) | | state' = state override { c |-> thetaABSM' } | ----------- So DeleteFile /\ phiABSM is a schema which describes the deletion of a file fn? in an abstract machine c. For tidiness, we can hide the components of ABSM and ABSM': DeleteFile1 = Exists ABSM; ABSM' . (DeleteFile /\ phiABSM) This style avoids the need for fancy decorations, and the question of ordering doesn't come up at all - except to say that if C = 1..n then state is in fact a sequence of abstract machine states. ------------------------------------------------------------------------ From: Derek H.Barnes (on UK.MOD.RSRE) Date: Tue, 20 May 86 13:57 GMT Subject: Z and Auto-G Folks, Any chance of an Auto-G like representation (or front end) for Z so that us simple minded ('engineers' was used - but I don't like oily hands) individuals could understand it ???? - - - - - Auto-G is a computer-aided system which 'implements the graphical design language G, whose simple, easily-learnt symbology enables any functional concept, however complex, to be clearly, completely, and unambiguously represented in the form of G diagrams'. (Quote from Auto-G sales handout.) The point is that G symbols show graphically how different parts of the system are related to one another, which some people find easier to follow than Z's mathematical abstraction. Editor. ------------------------------------------------------------------------ From: Trevor E G King (on UK.MOD.RSRE) Date: Fri, 30 May 86 12:29 GMT Subject: Miscellaneous Queries Here are three questions which are probably trivial but certainly irritating: (1) Given sets A,B,C, where A is a subset of B, and given the declaration f : B-->C, is it ok to write the term f(a), where a:A ?? (2) Given S = [(p,q):PxQ], may I write s.p or s.q, where s:S ?? If not, then how do I access the components of a tuple value?? (3) Given T = [a:A; b:B; c:C; ...] and t$sub$1, t$sub$2 : T, it seems natural to write a$sub$1, a$sub$2, etc, rather than t$sub$1.a, t$sub$2.a, etc. Are there any objections to the use of this syntactic equality ?? One response to (3) might be that in the presence of the schemas T$sub$1 or T$sub$2 the proposed decoration of the variables would be ambiguous. However, I can't see why (1) and (2) can't be allowed. Any help would be appreciated. An additional question: (4) Given S = [a:A; b:B]; T = {tuple S : AxB}, may I write t.a, where t:T ?? ------------------------------------------------------------------------ From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Fri, 30 May 86 12:16 GMT Subject: Word Processing Z At the meeting of implementers of Z on 24th April, it was agreed that a standard electronically mailable notation for Z would be included in the paper on a concrete syntax for Z being written by Steve King at Oxford. ------------------------------------------------------------------------ From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Fri, 30 May 86 11:32 GMT Subject: Reminder of Bibliography This is just a reminder of the note in Issue 5 of the Z Forum, asking you to send me a note of any publications which you know of relating to Z, so that they can be collected into a bibliography. Thanks. ------------------------------------------------------------------------ From: Ruaridh Macdonald (on UK.MOD.RSRE) Date: Mon, 2 Jun 86 11:09 GMT Subject: Mailing List The mailing list for the Z Forum is still expanding. If you know anyone else who wishes to be added, let me know (RM @ UK.MOD.RSRE). The current list of those who receive the Forum DIRECTLY is (I hope I have people's details correct): At the Programming Research Group in Oxford, the Forum goes into Unix News: INCOMING-ZFORUM @ UK.AC.OXFORD.PRG.SEVAX Martyn Andrews TSL ANDREWS @ TSLC Derek Barnes RSRE DHB @ UK.MOD.RSRE David Bosomworth Racal ITD DRFB @ ALVEY Peter Bottomley RSRE PCB @ UK.MOD.RSRE David Bounds RSRE DGB @ UK.MOD.RSRE Brian Bramson RSRE BDB @ UK.MOD.RSRE Alan Brown Newcastle University ALAN @ UK.AC.NEWCASTLE.CUSHAT Bernard Cohen Surrey University UK.AC.SURREY.EE!BERNIE @ UK.AC.READING David Freestone British Telecom BTFM @ ALVEY Richard Granville RSRE RJG @ UK.MOD.RSRE Nigel Haigh Racal ITD NPHH @ ALVEY Anthony Hall Systems Designers JAH @ UK.CO.SYSDES Ian Hayes Queensland University IANH % UQCSPE.OZ @ UK.AC.UKC Peter Hitchcock Newcastle University PETER @ UK.AC.NEWCASTLE.CUSHAT Roger Jones ICL Defence Systems RBJ % STL @ UK.AC.UKC Trevor King RSRE TEGK @ UK.MOD.RSRE Ruaridh Macdonald RSRE RM @ UK.MOD.RSRE Peter Marron GEC Computers MPJM % B5 @ GECD John McDermid Systems Designers JAM @ UK.CO.SYSDES Jogesh Naik Imperial Software Technology JN % UK.CO.IST.ISIS @ UK.AC.UKC Colin O'Halloran RSRE CMOH @ UK.MOD.RSRE Chris Paine Imperial Software Technology CMP % UK.CO.IST.ISIS @ UK.AC.UKC Ann Petrie Newcastle University ANN @ UK.AC.NEWCASTLE.CUSHAT Andrew Ricketts Racal ITD ADWR @ ALVEY Chris Sennett RSRE CTS @ UK.MOD.RSRE Dan Simpson Alvey Directorate DSAV @ ALVEY Susan Stepney Marconi Research Laboratories STEPNEY % MRC @ ALVEY Phil Terry TSL Ray Weedon Newcastle University RAY @ UK.AC.NEWCASTLE.CUSHAT Simon Wiseman RSRE SRW @ UK.MOD.RSRE ************************** END OF Z FORUM 1.6 **************************