Introducing the Whiley Cheat Sheet!

Recently, I created a Whiley Cheat Sheet for use in our SWEN224 course and I thought it was useful enough to share! The goal of the cheat sheet is to provide some simple examples to help you get going, rather than provide a comprehensive reference. I tried to cram as much as I could . . . → Read More: Introducing the Whiley Cheat Sheet!

Whiley v0.3.28 Released!

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!

Whiley v0.3.27 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!

Whiley v0.3.26 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!

Loop Variant Relations

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

Understanding Ghost Variables in Software Verification

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

Whiley v0.3.25 Released!

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!

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