🚀 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