Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!sdd.hp.com!hplabs!hpcc05!hpcuhb!hpindda!collin From: collin@hpindda.cup.hp.com (Collin Park) Newsgroups: comp.specification Subject: Re: VDM vs Z notation? Message-ID: <48050004@hpindda.cup.hp.com> Date: 13 Jun 91 23:03:34 GMT References: <48050001@hpindda.cup.hp.com> Organization: HP Information Networks, Cupertino, CA Lines: 185 Many thanks to all who replied to my earlier posting asking for a VDM vs Z comparison. Below is, in no particular order, the material relevant to VDM/Z comparisons. The postings have been excerpted/ edited/etc. and thus may not fully reflect the opinions of the authors to whom they are attributed. In my original posting I unfortunately used the phrase "standardizing VDM" when I should have said that the UK is "developing a standard for VDM," which would probably have caused less confusion. ------------------------------------------------------------------------------ Sean Matthews (sean@castle.ed.ac.uk) writes: Yes the UK is developing a standard for VDM, which may become an EC standard at least. I have, though, heard stories from people who might be entitled to an opinion, that the standard is being produced by people who do not entirely understand what they are doing --- i.e., there is a great deal more emphasis on syntax than semantics, to such an extent that the semantics may not be complete or coherent. Z, on the other hand, 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). But, having said that, other parts of Z, are extremely elegant, and natural, such as the way systems are designed by gradually constraining a set of objects --- and it looks great on a page :-) 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. VDM is closer in style to the languages that it will eventually be targetted on --- such as Pascal, ADA, PL/1, C, etc. And I think that this makes it much easier to convert a specification in VDM into a program (Z seems to me more of a specification, than a full development, language). It is also, I would imagine, much easier for most CS people to come to terms with than Z. Also, I suspect (without concrete evidence) that there is a much larger user base for VDM --- which is, incidentally, an IBM development itself. In short, I think (with some reservations about some aspects) that Z is much `nicer': more elegant and (in an informal, not formal sense) expressive. But I would probably go with VDM if I was developing a real, big, program. ============================================================================== Anonymous: To make a long story short - from my perspective, I think that you should definitely look at both techniques. However, note that once a specification is in VDM or Z, there really is no specific series of transformation steps proposed by either of the two methods to get a working system. It depends on your skill and knowledge. VDM will give you more suggestions as to what to do than Z, though. ============================================================================== Mike Lutz (mjl@cs.rit.edu): ... it is true that Z has been used at IBM's Hursley Labs to specify *part* of CICS. At the formal methods tutorial at ICSE 91 a couple of weeks ago, Mark Ardis and Susan Gerhart said something like 47K statements (out of 1M statements) had been so specified -- apparently IBM reverse engineers a specification the first time a module is modified as part of a new release, and from then on use this spec. to track the evolution of the module. As for VDM: yes, it is being standardized, but so is Z (though Z is a bit further behind). Also, VDM is showing its age: it still does not have a good ``structuring method'' to help scale up specifications. Remember: VDM is really a form of denotational semantics in disguise, originally developed to specify the semantics of programming languages. Right now, I'd favor Z, for two reasons: 1. The schema calculus gives an elegant solution to the scaling problem, and also supports separating the ``standard'' and ``exception'' cases in the specification. 2. Z is entirely based on sets. Everything -- functions, relations, bags, sequences -- are simply sets with special defining properties. This is not merely elegant, it is also very powerful, for all the set operators are available at any time when constructing specifications out of existing parts. VDM, by comparison, has many more ``primitive'' type constructors: in particular, functions are disjoint from sets. ============================================================================== Pat Place (prp@sei.cmu.edu): My preference is for Z over VDM. Yes, Z has been used by IBM on CICS, also by Tektronix for the development of software for an oscilloscope and in the specification of a heart pacemaker - these are the examples I can think of directly. VDM has been used for the specification of compilers and other software artifacts (databases,...) as well as parts of the control system for a nuclear power plant. Again, the list is actually longer but it is no longer possible to enumerate all specifications. Why do I prefer Z over VDM, in essence the two languages are similar in that they both use set theory and predicate calculus as their basis. Z does have good structuring facilities - the schema calculus is very powerful for putting pieces of specification together, though there can also be some problems - too many small pieces of specification and it can be hard to understand precisely what you have. The British standardisation effort has probably done more harm to VDM than good - though that is my opinion and you will find others who differ. ============================================================================== Anonymous: Z has been used in a number of systems including CICS and the specification of the Inmos floating point unit. I would not say (hope!) that the UK is standardizing on VDM. If anything there are many more Z users in the UK than VDM. For my own part I teach Z in a university and have taught and used Z in industry. I would claim that Z's real strength is for very high level specification and then refinement to code. VDM on the other hand is better for design level work and proof of properties of that design and the resulting code. ============================================================================== Tom Sarver (tsarver@andersen.com) I have used Structured Analysis Design Technique (SADT) which I hear is extremely similar (as in "name-change" similar) to VDM. As its name implies, SADT applies structured analysis and and top-down functional decomposition to a problem in a well-defined methodology. I believe that it is most applicable to commercial and industrial use because the assumption is that one has a clear idea of the whole system before starting. It also requires less training to read and understand than does Z. This feature makes it easier to use as a communication medium with a user community. My knowledge about Z comes strictly from the IEEE Software articles you cited. It appears to be based on extensions of first-order predicate logic, with some internal consistency rules. This appears to more applicable to the real-time arena because one can describe the objects in the system (and their interactions) without having full knowledge of the system as a whole. Such a system is very difficult to model using top-down design techniques. ============================================================================== Mark S Madsen IMHO, Z is quite neat, VDM is pretty creaky. But I'm not an expert on either. The main point of me replying is this: Z has very little to do with either of these orientations. Properly state-oriented methods, such as Petri nets or Estelle are either intractable (the former) or dead (RIP the latter). Event oriented specifications are (probably) best served by LOTOS (or CCs or CSP), but the real-time aspects haven't been hammered out yet for process algebras (this is my main research branch at present). LOTOS is really the way forward, though, just because of the amount of effort going into using, testing, and extending it. These both sound like malicious rumours :-) Standardising on VDM??? Someone is joking with you. I can tell you that BT (formerly British Telecom) has standardised on LOTOS and Z. ============================================================================== jeff scott (jscott%mandata@uunet.uu.net): One book you might want to read is 'Case Studies in Systematic Software Development' by Jones and Shaw, Prentice Hall international series. It's mainly about application of VDM to various design problems. I visited Roger Shaw last year and he seems to feel that Z and VDM each have their own strengths and weaknesses but that Z was probably better for a majority of design problems one is likely to encounter. ============================================================================== Again thanks to all who responded. Collin Park