Recently, I encountered what I thought was a bug in the Whiley Compiler. The issue related to the current treatment of do/while loops and loop invariants. Having now spent a fair bit of time researching the issue, the answer is not so clear.
The problem manifested itself when I tried to verify the following . . . → Read More: Loop Invariants and Do/While Statements
Well, it’s time for yet another release of the Whiley compiler. This one is fairly low key, focusing primarily on bug fixes. Specifically, these issues have been resolved:
#346 — Temporary Fix for Unsuported Bytecodes in the Verifier. #341 — Temporary Fix for Verifying Method Types. #338 — Fix for handling record constants in . . . → Read More: Whiley v0.3.24 Released!
In this article, I’ll look at some interesting issues relating to the use of break statements within loops, and how this affects the idea of a loop invariant. For some general background on writing loop invariants in Whiley, see my previous post. To recap the main points, here’s a simple function which requires a . . . → Read More: Loop invariants and Break Statements