collin@hpindda.cup.hp.com (Collin Park) (05/30/91)
Greetings,
I posted the following on comp.software-eng, and someone suggested I post
here also, where I probably should have posted it in the first place?
Unless I hear otherwise, I'll post the summary in comp.software-eng and
just put a pointer in this notesgroup. Thanks for your input...
collin
===============================================================================
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.
I understand that Z has been applied to some parts of IBM's CICS, and
that it has also been used to specify a real-time kernel. (The latter
is especially of interest to me, since many programming aids seem to
lack facilities for state-oriented or event-driven design.)
On the other hand, I also hear that the UK is in some way standardizing
VDM, and some say that VDM is the notation best suited to industrial
application.
Any thoughts, opinions, case histories...? Please email me and I will
summarize here. Thanks.
Collin Park
collin@hpinddu.cup.hp.com
...!hplabs!hpinddu!collinstg@cs.ed.ac.uk (Stephen Gilmore) (05/31/91)
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
collin@hpindda.cup.hp.com (Collin Park) (06/06/91)
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
collin@hpindda.cup.hp.com (Collin Park) (06/14/91)
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 Parkmike@prg.ox.ac.uk (Mike Spivey) (06/17/91)
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
elc@fmg.bt.co.uk (Elspeth Cusack) (06/18/91)
Mark S Madsen <msm@computing.lancaster.ac.uk> , quoted by collin@hpindda.cup.hp.com (Collin Park @ HP Information Networks) said: 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. This statement about BT interest in formal methods is a little misleading. It is true that there is research activity in both LOTOS and Z,and that these are our `favoured candidates' (as researchers) for specifying distributed systems. But that is a long way from saying that the company has standardised on LOTOS and Z! BT also has an active community of SDL users in the protocol testing field, and considerable involvement with software methodologies and development conventions. Elspeth Cusack
msm@comp.lancs.ac.uk (Mark S Madsen) (06/19/91)
In article <1991Jun18.152454.27474@fmg.bt.co.uk> elc@fmg.bt.co.uk (Elspeth Cusack) writes: >Mark S Madsen <msm@computing.lancaster.ac.uk> >, quoted by collin@hpindda.cup.hp.com (Collin > Park @ HP Information Networks) said: (I apologise in advance for any inconsistencies that may arise through my not having ever seen Collin's quotation of my email to him.) >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. Sounds like my sort of self-assured tone, so it was probably I that wrote it :-) >This statement about BT interest in formal methods is a little >misleading. It is true that there is research activity in both ^^^^^^^^^^ Oh, definitely it must indeed have been I writing, if the content is misleading! >LOTOS and Z,and that these are our `favoured candidates' (as >researchers) for specifying distributed systems. But that is a >long way from saying that the company has standardised on LOTOS >and Z! BT also has an active community of SDL users in the >protocol testing field, and considerable involvement with >software methodologies and development conventions. My apologies to everyone at BT for misrepresenting them to the world. (I am not apologising for misleading the net because the above quote was sent in private email, and quoted without permission from me.) I was clearly under a mistaken impression that LOTOS and Z were in possession of official approval. However (I love having the opportunity to begin a paragraph with that word :-), let me emphasise that at least one point in my original posting was correct, and is implied in Elspeth's posting: VDM is by no means the only formal technique in use in the UK with either business or academic concerns. >Elspeth Cusack Hope you're all keeping well down there - say hi to Steve from me. Mark -- ______________________________________________________________________ Mark S Madsen +44-524-65201x3819 msm@comp.lancs.ac.uk Department of Computing, Lancaster University, LA1 4YR, UK ______________________________________________________________________
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