It’s about time for another release of Whiley. This represents some interesting developments, though I continue to struggle with debugging and improving verification. The main highlights for this release are:
Improved wyal file parser. This is responsible for parsing wyal files and feeding them into the code generator. Previously, the parser was very simplistic, . . . → Read More: Whiley v0.3.26 Released!
Proving that a loop always terminates is a common requirement when verifying software. The usual approach to doing this is to provide a loop variant function. This is typically an integer expression which decreases on every iteration of the loop. Consider the following loop:
function contains([int] items, int item) => bool: int i = . . . → Read More: Loop Variant Relations
Verification tools often support the use of ghost variables to help in the verification process. A ghost variable is not needed for the program to execute, and will not be compiled into object code. Typically, they are declared with a ghost modifier or similar, but are otherwise identical to normal program variables (i.e. they . . . → Read More: Understanding Ghost Variables in Software Verification
Time for another release of the Whiley compiler. This is relatively low key, though includes the first steps towards an improved bytecode API (see #190). There are also a range of bug fixes for various minor issues:
Refactoring wyil.lang.Code and wyil.lang.CodeBlock. In order to support proper nested bytecode blocks, I am refactoring the WyIL . . . → Read More: Whiley v0.3.25 Released!
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
Another update to the Whiley compiler has just been released. This is a fairly small update, consisting primarily of bug fixes. The only significant change was:
Type checker now respects a variable’s declared type. Previously, the declared type was ignored as discussed here.
As usual, you can get the latest files below. Furthermore, you . . . → Read More: Whiley v0.3.23 Released!
Last week, my CrazyFlie nano-quadcopter finally arrived and, since then, I’ve been learning how to fly! The copter is much smaller than I was expecting, and it requires you to solder a few bits together.
At first, I had a lot of problems trying to fly it. After a lot of fairly major . . . → Read More: Flying the CrazyFlie Quadcopter!
After the recent release of Whiley v0.3.22 which updated the language syntax, I have now updated the Eclipse plugin accordingly. See this page for more on installing the plugin from within Eclipse.