checkedint call removal

[bearophile via Digitalmars-d]

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