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
I have started to read those pages, it looks interesting. From
one of the first links (Sudoku solver):
valid values are 0..9. 0 denotes an empty cell
predicate valid_values (g:grid) =
forall i. is_index i -> 0 <= g[i] <= 9
So can't they represent that the value 0 is an empty cell in the
code instead of comments? (I think this is possible in Ada
language).
It's a bit sad that D1 has removed the literate programming
feature of D1. In Haskell it's used all the time.
Bye,
bearophile
