sean@castle.ed.ac.uk (S Matthews) (06/19/91)
Colin Park reports me as saying that: >> But Z could be accused of having other problems: for instance some >> aspects of the notation (the part involving decoration of schemas and >> variables, is to my mind, a bit dodgy --- to say the least). To which Mike Spivey retorted, slightly hurt perhaps: > I don't understand how Z can have a "fairly good" semantics, and yet > have such basic parts of the notation be "a bit dodgy --- to say the > least". In fact, it is a major goal of the semantics to clear up > exactly what is the meaning of decoration and other operations on > schemas. Perhaps Sean Matthews would explain what he thinks is the > problem here? What Colin Park left off from my message was a rider saying that it was a quick collection of thoughts put together while I was doing something else. But anyway, what do I mean? I was using the word dodgy in an `informal' sense, while Mike takes it that I am using it in a formal sense. I meant that it perhaps obscures, rather than that it is obscure. It is necessary but not sufficent that a formal specification language have a semantics. Turing machines are well understood, so are PRA, PA and ZFC. If that were all that was needed, then any of them could be used equally effectively as a specification language. A specification language is used to keep large (though usually fairly simple) mathematical structures under control, and most of the design work should be to make that easier. My complaint about Z is that some of it is not well designed to make specification easier, in the informal sense that it does not work in a way that I think is intuitive or the `right way'. It really boils down to `I do not like the way this is done', like e.g., `I do not like the way variable scoping is handled in Cobol'. Take, for instance, the line in the introduction of chapter 5 of the Z reference manual that goes: `This chapter explains the conventions which allow us to use these structured mathematical theories to describe computer programs.' My problem is with the word `convention'. The bits of Z that turn it into a language for specifying computer systems are only conventions, so, to model a procedure, the input parameters are marked ?, and the output parameters are labeled !. The whole thing feels ad hoc. >> Also, VDM has better facilities for structuring very large >> specifications --- the notion of variable scope is a bit woolly in >> Z. It is there, but it is not so clear, and the user has to do >> more explicitly. > In fact, ZRM as described in Jones' books has NO facilities for > structuting large specifications (though some were considered by the > standards effort). Again, I'd be grateful for some indication of how > a "fairly good" semantics can leave the notion of variable scope "a > bit woolly". What I was thinking of here was the lower level of structuring, rather than 500 page systems. I do not think either Z or VDM has very good facilities for really large scale specs, but in the small, at least, VDM has the advantage as follows: In VDM, a data structure is defined D is X : T, <invariant on D> all at once, nothing more to be said. On the other hand, in Z it is easy to write D is X:T and P(D) is the invariant . . five hundred lines of text. . Oh, and by the way, P'(D) is an another invariant. I think this is a problem, especially since the way schemas are presented makes them look like boxes that delimit the specification of that structure. I think this is a comparative win for large scale specifications, since it means that at least the local structure of the system is defined locally. I have other small complaints. None of them are really substantial, but the general effect is to make me feel that Z is not as well designed as it could be. In general, I feel about Z the way someone contemplating Algol 60 in 1962 might feel, i.e.,: `This is great. But that call by name mechanism, and the lack of standard i/o facilities, and...' And, to continue (and maybe force a bit) the analogy for VDM, someone contemplating Fortran at the same time might feel: `Compared to Algol 60, this is horrible, but I can probably get more work done with it. My programming team will understand it, for one thing.' And to round things off with algebraic specs, someone will sidle up and add: Well I think both of them look pretty horrible compared to thiss great new language called Lisp' Z is a nice language, which I like quite a lot, and use it for bits of work, but it is not the last word (though I think it is a good first or second word), and I am looking forward to Z++, or Z-68 (though, on second thoughts...). Sean Matthews 80 South Bridge, Edinburgh, UK Dept. of Artificial Intelligence +44 (0) 31 650 2722 University of Edinburgh sean@castle.ed.ac.uk -- Sean Matthews 80 South Bridge, Edinburgh, UK Dept. of Artificial Intelligence +44 (0) 31 650 2722 University of Edinburgh sean@castle.ed.ac.uk