checkedint call removal
via Digitalmars-d
digitalmars-d at puremagic.com
Wed Jul 30 13:22:00 PDT 2014
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
The advantage of formally separating what is proven from what is
to be proved is quite obvious. You can generate annotated
bindings for libraries and frameworks that can both increase
correctness and provide semantic information that can be relied
on (for optimization and other purposes).
More information about the Digitalmars-d
mailing list