On 07/31/2014 01:32 PM, bearophile wrote:
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
It is not an inherent issue with verification. One way to avoid this is to allow correctness proofs to be done in a separate place.
