🚀 go-pugleaf

In <1992Sep29.092813.19695@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

I think the major advantage Z/VDM have over the Dijkstra methods is
that Z/VDM have a better PR machine.  Any formal technique is so
much better that the way software is developed now that it really
doesn't matter which one you use as long as the notation is a good fit
to your task.

>In those books in fact not so much attention is paid to specifications
>as to proofs of correctness. Is this the main difference?

The Dijkstra methods focus more on developing an appropiate notation
(one that fits your task), elegant solutions in a mathamatical sense,
and a checkable proof.  These methods do *not* imply you can
prove anything correct.  I guess the best you can hope for is a
correct proof and derivation of code.

--- eric
-- 
HOME: esj@harvee.billerica.ma.us  HAM  ka1eec
WORK: 617.630.4687 (w)   esj@ruby.polaroid.com
source of the public's fear of the unknown since 1956