Articles

Understanding Effective Unions in Whiley

The concept of effective union types in Whiley exposes some interesting features worth considering.  In particular, they result in a separation between the readable and writeable view of a type.  But, we’re getting ahead of ourselves!  Let’s start with what exactly effective unions are…

Effective Unions

An effective union is a union type which . . . → Read More: Understanding Effective Unions in Whiley

Encoding C Strings in Whiley

In this post, we’re going to consider representing the classic C string in Whiley. This turns out to be useful as we can then try to verify properties about functions which operate on C strings (e.g. strlen(), strcpy(), etc). If you’re not familiar with C strings, then the main points are:

Roughly speaking, C . . . → Read More: Encoding C Strings in Whiley

Verifying Software with Whiley

A couple of weeks back, I gave a presentation to the Wellington Java User Group. The talk provides a useful introduction to verifying software in Whiley, and shows a bunch of interesting examples. Anyway, you can see the presentation here:

Wellington Java User Group Presentation from John Hurst on Vimeo.

. . . → Read More: Verifying Software with Whiley

Verification with Data from Untrusted Sources

Recently, I was listening to the latest edition of the Illegal Argument podcast, and it turns out they were discussing Whiley! (about 103:16 minutes in). The discussion was about how verification interacts with data from an untrusted source (e.g. from a database, network connection, etc). In particular, whether or not we can safely feed . . . → Read More: Verification with Data from Untrusted Sources

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!

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

Iso-Recursive versus Equi-Recursive Types

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, what does all this mean? Well, let’s look at an example:

define IntList as . . . → Read More: Iso-Recursive versus Equi-Recursive Types

Compile-Time Verification and I/O

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 int where $ >= 0 define pos as int where $ > 0 define . . . → Read More: Compile-Time Verification and I/O

Whiley Puzzler #1

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