The latest release is upon us, after a short break whilst I was holidaying in Europe! This includes a few simple bug fixes and updates (see #433 and #392), along with one significant feature:
Improved Context Information for Verification Errors (#435). When a verification error occurred, it was often difficult to tell which part . . . → Read More: Whiley v0.3.31 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!
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
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!
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!
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