🚀 go-pugleaf

In article <48050004@hpindda.cup.hp.com> collin@hpindda.cup.hp.com
(Collin Park) reports that Sean Matthews (sean@castle.ed.ac.uk)
writes:

   Z ... has a fairly good semantics produced by Mike Spivey, once you
   get over the notion of a semantics for Z in something that looks so
   much like Z.  But Z could be accused of having other problems: for
   instance some aspects of the notation (the part invoving decoration
   of schemas and variables, is to my mind, a bit dodgy --- to say the
   least).

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?  Later, he says,

   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".

-- Mike Spivey