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:
holds on entry to the loop; holds after the loop body is executed; holds when the loop finishes.
Loop invariants can be tricky to . . . → Read More: Understanding Loop Invariants in Whiley