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