Loop Invariants and Do/While Statements

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

Whiley v0.3.24 Released!

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!

Loop invariants and Break Statements

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