By redjamjar
via whiley.org
Submitted: Jan 28 2013 / 15:36
In this article, I'll look at a common problem one encounters when verifying programs: namely, writing loop invariants. In short, a loop invariant is a property of the loop which: (1) holds on entry to the loop; (2) holds after the loop body is executed; (3) holds when the loop finishes.
Tweet
SaveShareSend
Tags: java, open source, other languages, research
Add your comment
