|
|||||
|
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 |
 |
||||
|
Copyright © 2020 David J. Pearce - All Rights Reserved 53 queries. 0.313 seconds. |
|||||
