Re: Advantages of Z and VDM over Dijkstra-style specifications?

Article View: comp.specification

Article #266

Back to comp.specification Previous Next

#266

From: Conrad Cunningham
Date: Thu, 01 Oct 1992 13:00

25 lines
1835 bytes

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

Technical Details

Message-ID: <1992Oct1.130011.28848@cs.olemiss.edu>

Path: arc1-ca.pugleaf.net!sparky!uunet!gatech!concert!duke!sam.cs.olemiss.edu!hcc

References: <1992Sep29.092813.19695@ghost.dsi.unimi.it> <6288@m1.cs.man.ac.uk>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!sparky!uunet!gatech!concert!duke!sam.cs.olemiss.edu!hcc
From: hcc@cs.olemiss.edu (Conrad Cunningham)
Newsgroups: comp.specification
Subject: Re: Advantages of Z and VDM over Dijkstra-style specifications?
Message-ID: <1992Oct1.130011.28848@cs.olemiss.edu>
Date: 1 Oct 92 13:00:11 GMT
References: <1992Sep29.092813.19695@ghost.dsi.unimi.it> <6288@m1.cs.man.ac.uk>
Organization: University of Mississippi, Dept. of Computer Science
Lines: 25

Reply to Parent Message