On software quality and engineering

Martin Schwenke martin at meltin.net
Tue Nov 5 09:26:14 EST 2002


>>>>> "Alex" == Alex Satrapa <grail at goldweb.com.au> writes:

    Alex> Now, can anyone give me the ISBN for a good reference or
    Alex> tutorial book on Z formal proof?

Z is a good specification language because it has nice structuring
capabilities.  However, the "Z to code" thing is still harder than
some of the alternatives.

A good alternative is "The Refinement Calculus", which involves
writing precondition/postcondition specifications and using a calculus
to transform those specifications into programs.  Note that the
transformations aren't automatic...  :-) The refinement calculus was
independently thought up by Carroll Morgan, Ralph Back and Joe Morris,
so it must be good.  :-)  A good book on the topic is Carroll Morgan's
"Programming from Specifications", now out of print, but available
via:

  http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/

Carroll is one of the smartest people I've ever met.  Among other
things, I saw him give a really neat presentation about formalising
"gotos" (well, "exits", but they accomplished the same thing), even
though they're considered quite harmful...  :-)

peace & happiness,
martin



More information about the linux mailing list