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.
The next release of Whiley is now available. This implements some significant changes to the language syntax, as discussed in this post and this post. Although the migration towards this new syntax is not fully complete, it is largely working well. Specifically, the main changes in this release are:
Draft Language Specification. Perhaps one . . . → Read More: Whiley v0.3.22 Released!