🚀 go-pugleaf

Collin Park of HP labs writes in article 261 of comp.specification:

> Anyone have any comments on the utility of Z vs VDM?  Several articles
> using the Z notation appeared in last September's IEEE SOFTWARE magazine,
> and reviews of two books ("Systematic Software Development Using VDM, 2/e"
> and "Z: An Introduction to Formal Methods") appeared in the last two 
> issues.  

My PhD thesis is a critical evaluation of Z, VDM and algebraic specifications.  
It is centered around the rigorous development of a specification translator with 
the specifications given in Z, VDM and ASL.  Several refinement techniques are
used: these range from classical VDM development to an original transformational 
approach to implementing from a Z specification.  Advantages and disadvantages
of the approaches are discussed.  Also, the correctness and efficiency of the 
completed implementation are assessed.  The implementation is in an imperative
programming language and is approximately 10,000 lines long.

Copies of the thesis are available from:

            Dorothy McKie
            Laboratory for Foundations of Computer Science
            Department of Computer Science
            The James Clerk Maxwell Building
            The King's Buildings
            University of Edinburgh
            Edinburgh EH9 3JZ,  UK.            

            Tel:   031-650-5175
            Email: dam@uk.ac.ed.lfcs

The details of the thesis are:

            Title:   Correctness-Oriented Approaches to
                     Software Development
            Author:  Stephen Gilmore
            Pages:   168
            Report:  CST-76-91 (also ECS-LFCS-91-147)
            Price:   8 pounds

An up-to-date list of all LFCS publications (reports and PhD theses) can be obtained 
from Dorothy McKie at the address given above.


Stephen Gilmore

Laboratory for Foundations of      JANET: stg@uk.ac.ed.lfcs
  Computer Science                 UUCP:  ..!mcvax!ukc!lfcs!stg	
Department of Computer Science     ARPA:  stg%lfcs.ed.ac.uk@nsfnet-relay.ac.uk
The James Clerk Maxwell Building
The King's Buildings
University of Edinburgh
Edinburgh EH9 3JZ,  UK.            Tel:   031-650-5145

Stephen Gilmore writes:

> My PhD thesis is a critical evaluation of Z, VDM and algebraic
> specifications...
> [...]

> The details of the thesis are:

>             Title:   Correctness-Oriented Approaches to
>                      Software Development
>             Author:  Stephen Gilmore
>             Pages:   168
>             Report:  CST-76-91 (also ECS-LFCS-91-147)
>             Price:   8 pounds

For U.S. readers, Ms McKie will accept U.S. funds:  $16.00

-collin

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 <msm@computing.lancaster.ac.uk>

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

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