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