Re: VDM vs Z notation?

Article View: comp.specification

Article #437

Back to comp.specification Previous Next

#437

From: Stephen Gilmore
Date: Fri, 31 May 1991 16:07

52 lines
2813 bytes

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

Technical Details

Message-ID: <11795@skye.cs.ed.ac.uk>

Path:

arc1-ca.pugleaf.net!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

References: <48050001@hpindda.cup.hp.com>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!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

Reply to Parent Message