Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!nstn.ns.ca!news.cs.indiana.edu!att!linac!uwm.edu!zaphod.mps.ohio-state.edu!wuarchive!uunet!mcsun!ukc!edcastle!cs.ed.ac.uk!stg
From: stg@cs.ed.ac.uk (Stephen Gilmore)
Newsgroups: comp.specification
Subject: Re: VDM vs Z notation?
Keywords: VDM, Z, ASL, specification, refinement, implementation
Message-ID: <11795@skye.cs.ed.ac.uk>
Date: 31 May 91 16:07:00 GMT
References: <48050001@hpindda.cup.hp.com>
Sender: nnews@cs.ed.ac.uk
Organization: Department of Computer Science, University of Edinburgh
Lines: 52

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