🚀 go-pugleaf

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