The next release of Whiley is already upon us, after only a week or so since the last. This release consists of a slew of minor bug fixes, many of which have been discovered through students using the system in practice. The main items are:
Problem Generating JVM Bytecode (#415). This related to compiling . . . → Read More: Whiley v0.3.28 Released!
The next release of Whiley is upon us. This includes a large number of bug fixes, and a significant rewrite of the verifier. Unfortunately, the verifier is not yet verifying many more examples, but it’s now placed to do so. Specifically, the main highlights are:
Better Support for Contractive Types. Contractive types are those . . . → Read More: Whiley v0.3.27 Released!
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!