Ola Fosheim Grøstad:
Here is a set of examples of annotated programs that have been
formally proved correct for those interested:
http://toccata.lri.fr/gallery/why3.en.html
More comments:
-------------------
A problem with code like this is that it's drowing in noise. The
precondition/invariant/variant code in the 't3' function is
obscuring what the code is actually doing on the data:
http://toccata.lri.fr/gallery/queens.en.html
One way to solve this problem: the editor has to show the testing
code with a different background color (and collapse it away on
request).
(And I'd like to read the "More realistic code with bitwise
operations").
-------------------
I have added a third version here:
http://rosettacode.org/wiki/Dutch_national_flag_problem#More_Verified_Version
Adapted from:
http://toccata.lri.fr/gallery/flag.en.html
D lacks the pre-state (old a) and (at a 'Init), the loop
variants, the loop invariants (despite D has a invariant keyword
used for struct/classe invariants), ghost variables (I have used
'riPred' and 'aInit' for the loop variants and invariants. I have
used a debug{} to simulate them in D), and writing the
post-condition was a bit of pain.
Bye,
bearophile
