Whiley Compiler (WyC)

The Whiley programming language uses union types as a way of combining types together.  Here’s a simple example to illustrate: null|int indexOf(string str, char c): for i in 0..|str|: if str[i] == c: return i // found a match // didn't find a match ... [More] return null Here, the type null|int is a union type . . . → Read More: Understanding why Union Types are useful [Less]

As the Whiley compiler continues to evolve, certain aspects of its architecture are really starting to mature.  One of the more recent pieces to take shape is the verification pipeline.  This is the process by which a Whiley file is converted into a ... [More] series of verification conditions, which are then checked by the automated . . . → Read More: The Architecture of Verification in Whiley [Less]

A few weeks ago, I was in Melbourne attending the Australasian Software Engineering Conference and, whilst I was there, I gave a talk on Whiley at the Melbourne Java Users Group. Well, here’s the talk … You can also get the slides from here!

Today, more then ever before, I/O dominates what software is about.  Of course, it’s always been important but, with increasing bandwidths, I/O seems to be what most programs now spend most of their time doing.  This leads to interesting questions ... [More] about how, for example, to handle millions and millions of concurrent connections and we . . . → Read More: Input / Output and the Object-Oriented Paradigm [Less]

It is with some disappointment that I’ve finally decided to release v0.3.19 despite this being almost 3 months overdue!  The disappointment arises because, despite a lot of valiant effort, verification is still not working very well — and, in fact ... [More] , is probably worse than the previous release!  However, on the other hand, I have . . . → Read More: Whiley v0.3.19 Released! [Less]

An important component of the Whiley language is the use of recursive data types.  Whilst these are similar to the algebraic data types found in languages like Haskell, they are also more powerful since Whiley employs a structural type system. So ... [More] , what does all this mean? Well, let’s look at an example: define IntList as . . . → Read More: Iso-Recursive versus Equi-Recursive Types [Less]

A surprisingly common question people ask me when I talk about compile-time checking of pre-/post-conditions and invariants is: how do you deal with I/O? To understand what the difficulty is, let’s consider a simple example in Whiley: define nat as ... [More] int where $ >= 0 define pos as int where $ > 0 define . . . → Read More: Compile-Time Verification and I/O [Less]

In this article, I’ll look at a common problem one encounters when verifying programs: namely, writing loop invariants.  In short, a loop invariant is a property of the loop which: holds on entry to the loop; holds after the loop body is executed; ... [More] holds when the loop finishes. Loop invariants can be tricky to . . . → Read More: Understanding Loop Invariants in Whiley [Less]

I was having an interesting discussion with a colleague today about various aspects of Whiley, and we came up with an interesting bit of example code which is something of a puzzler. Consider these two different versions of a function f(any): Version 1: int f(any x): if x is string: return g(x) else: return . . . → Read More: Whiley Puzzler #1

The next version of Whiley is upon us!  This consists of mostly lightweight improvements over v0.3.17 and various bug fixes (see issues for more).  I have now been attempting to verify some of the microbenchmarks in Wybench, with some useful progress ... [More] being made (although it is flushing out a lot of issues). ChangeLog Lots . . . → Read More: Whiley v0.3.18 Released! [Less]