Articles

Whiley v0.3.30 Released!

The next release of Whiley is now ready to be downloaded.  This includes a small number of bug fixes and two more significant changes:

#418 — Removal of implicit coercions.  This has some consequences for how you write Whiley programs, and there are probably some follow-on changes needed. #427 — Improved disambiguation of cast . . . → Read More: Whiley v0.3.30 Released!

A Story of Cast Expressions

Issue #427 “Bug with Dereferencing Array Types” seemed like just another bug.  Submitted by a user last week (@Matt–), I didn’t think too much of it.  But, as sometimes happens, appearances can be deceiving.  In this case, the bug identified a flaw in the syntax of Whiley with respect to the treatment of cast . . . → Read More: A Story of Cast Expressions

Whiley v0.3.29 Released!

The next release of Whiley is now ready to be downloaded.  This includes a number of bug fixes, along with a change in the WyIL bytecode format.  The latter is ahead of further planned changes to improve the bytecode format and verification.  The list of changes is:

#423 — Bug fix related to parsing . . . → Read More: Whiley v0.3.29 Released!

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!