🚀 go-pugleaf

In article <1992Sep29.092813.19695@ghost.dsi.unimi.it> vaccari@ghost.dsi.unimi.it (matteo vaccari) writes:
>
>I am new to formal specifications, and I am wondering about
>the advantages of using specification languages like Z or VDM
>over the kind of program specifications described in the books
>  "Predicate Calculus and Program Semantics" by E. Dijkstra,
>or
>  "Programming in the '90s", by E. Cohen
>
>In those books in fact not so much attention is paid to specifications
>as to proofs of correctness. Is this the main difference?

Z and VDM have evolved from "straight predicate calculus"
specifications as the need to specify larger systems has been
understood. Both Z and (the specification language part of) VDM employ
a collection of data types which make it easier to build abstract
models of systems.

It is certainly *not* true that VDM (the method) pays less attention
to proofs although I would emphasize their use in development rather
than post facto correctness proofs. See for example

	
@book{Jones90a,
	author	    =	"C. B. Jones",
	title	    =	"Systematic Software Development using VDM",
	edition =	{Second},
	publisher   =	"Prentice Hall International",
	year	    =	"1990",
	length =	"333 pages"
}

@book{JonesShaw90,
	editor =	"C. B. Jones and R. C. F. Shaw",
	title =		"Case Studies in Systematic Software Development",
	publisher =	"Prentice Hall International",
	year =		"1990",
	length =	"387 pages"
}

The situation with Z on development is more complex: the early books
were confined to specifications (and proofs about the specifications
themselves); more recently, many people use Morgan's "refinement
calculus".

An interesting discussion on the use of Z/VDM is in Hoare's Preface to


@book{VDM90,
	editor =	"D. {Bj\o rner} and C. A. R. Hoare
			and H. Langmaack",
	title =		"{VDM'90: VDM and Z} -- 
			Formal Methods in Software Development",
	publisher =	"Springer-Verlag",
	year =		1990,
	volume =	428,
	series =	"Lecture Notes in Computer Science"
}


cliff jones

In article <1992Sep29.092813.19695@ghost.dsi.unimi.it> vaccari@ghost.dsi.unimi.it (matteo vaccari) writes:
>>  "Predicate Calculus and Program Semantics" by E. Dijkstra,
>>or
>
>  "Programming in the '90s", by E. Cohen
>
>In those books in fact not so much attention is paid to specifications
>as to proofs of correctness. Is this the main difference?

It's probably true that not enough attention is given to specification
issues, but it is not really accurate to say that Cohen's book just
pays attention "to proofs of correctness."  I take that phrase to mean
"program verification", that is, the proof that an existing program meets its
specification.  The focus of Cohen's book is on program derivation (or
calculation or synthesis, choose your term) rather than ex post facto 
verification.  Program derivation is the use of correctness concepts
and various design heuristics to discover (i.e., derive, calculate, or
synthesize) a program that satisfies a given specification.  

- Conrad Cunningham, University of Mississippi, Computer & Information Science
-- 
-------------------------------------------------------------------------------
H. Conrad Cunningham  | Dept. of Computer & Info. Sci., Univ. of Mississippi
Tel:  (601) 232-5358  | 302 Weir Hall, University, MS 38677  U.S.A.
Fax:  (601) 232-7010  | Email:  cunningham@cs.olemiss.edu 

The specification style taught by the Z and VDM schools and the program
derivation methods taught by Dijkstra, Hoare, Gries, Cohen and many others
aren't in competition with one another - they are complementary.

The program derivation methods emphasize developing correct algorithms
from very short specifications - usually just a line or two of formulas.

The Z and VDM schools teach how to write specifications for large systems -
systems whose prose requirements documents can be hundreds of pages long.

The mathematical foundations for Z/VDM style specs and for Dijkstra/Hoare/etc.
specs are essentially the same: typed sets, relations, functions, arithmetic 
and first order logic.   This mathematics appears unadorned in the Dijkstra 
etc. specs, but Z and VDM provide additional constructs to help organize 
large (many pages long) formal specifications.

So, you can specify your (big) system in Z or VDM, and then when it comes time
to do the detailed implementation of some particular piece of it, you can
tweeze out the relevant formulas and use them in a Dijkstra (etc.) development.

An interesting issue concerns how to decide when it is useful/cost effective to
perform a rigourous Dijkstra (etc.) style development of the implementation.
Some argue that it is useful to produce a Z or VDM spec for descriptive
purposes, to guide a rather informal development of the implemention, without
going all the way through a full formal development of the implementation.

- Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle, USA