Articles

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

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

Thoughts on Writing Loop Invariants

As the Whiley system is taking better shape every day, I’m starting to play around more and discover things.  In particular, there are some surprising issues surrounding while loops and their loop invariants. These are things which I’ll need to work on in the future if Whiley is to stand any chance of being . . . → Read More: Thoughts on Writing Loop Invariants

The Architecture of Verification in Whiley

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 series of verification conditions, which are then checked by the automated . . . → Read More: The Architecture of Verification in Whiley

Understanding Loop Invariants in Whiley

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; holds when the loop finishes.

Loop invariants can be tricky to . . . → Read More: Understanding Loop Invariants in Whiley

Whiley Talk at Wellington JUG (VIDEO)

Last month, the Wellington Java User Group was kind enough to invite me to give a talk on Whiley.  The talk is a general introduction to Whiley, including the syntax, some issues related to implementation and inter-operation with Java.  The talk was video and, finally, after some faffing around I’ve uploaded it onto YouTube . . . → Read More: Whiley Talk at Wellington JUG (VIDEO)

Actor Syntax in Whiley

Recently, I’ve been doing some work on the syntax for [[Actor model|Actors]] in Whiley. After some deliberation, I’ve decided to go with explicit syntax for both synchronous and asynchronous message sends. This means any message can be sent either synchronously or asynchronously. Obviously, sending asynchronously is preferable. However, in cases where a return value . . . → Read More: Actor Syntax in Whiley

Normalising Recursive Data Types

Recently, I came across an interesting problem with the type system I’m using in Whiley.  Specifically, the problem relates to recursive types which are equivalent but not identical.  Consider, for example, the following Whiley code:

define Link as { int data, LinkedList next } define LinkedList as null | Link

This is a fairly . . . → Read More: Normalising Recursive Data Types

Short Whiley Demo [VIDEO]

I’ve put together a little demonstration of the Whiley language in use. The demo only covers the basic idea of Whiley and, in particular, demonstrates how the pre- and post-conditions work:

Anyway, this was a bit of fun for a Saturday afternoon. Turns out making videos is harder than I thought . . . → Read More: Short Whiley Demo [VIDEO]