Articles

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

Generating Verification Conditions for Whiley

Probably the most interesting aspect of the Whiley language is that it supports compile-time verification of preconditions, postconditions and other invariants.  There are two main aspects of how this works:

Generation of Verification Conditions (VCs) from the source code.  A verification condition is a logical expression which, if proved to be satisfiable, indicates an . . . → Read More: Generating Verification Conditions for Whiley

Flow Typing for References in Whiley

The Whiley language splits into a fully functional “core” and an imperative “outer layer”.  References and objects do not exist within the functional core.  However, they can exist within the imperative outer layer and are necessary for supporting state and other side-effecting computation.  Here’s a simple example:

define Buffer as ref { [int] items . . . → Read More: Flow Typing for References in Whiley

Illustrating Compile-Time Verification in Whiley

With the latest release of Whiley, compile-time checking of constraints can be enabled with a command-line switch.  So, I thought a few examples of this were in order.

Example: Absolute of an Integer

Consider this simple program:

define nat as int where $ >= 0 nat abs(int x): return x

This defines a type . . . → Read More: Illustrating Compile-Time Verification in Whiley

Variable Scoping for Try-Catch Blocks in Whiley

A friend of mine was talking about how variable scoping for try-catch blocks in Java really frustrated him sometimes.  Specifically, the problem was related to variables declared inside try blocks not being visible in their catch handlers. The example would go something like this:

int val; try { int tmp = f(); // cannot . . . → Read More: Variable Scoping for Try-Catch Blocks in Whiley

Termination of Flow Typing in Whiley

Whiley uses flow typing to give it the look-and-feel of a dynamically typed language (see this page for more on flow typing).  In short, flow typing means that variables can have different types at different program points.  For example:

define Node as { int data, Tree left, Tree right } define Tree as null . . . → Read More: Termination of Flow Typing in Whiley

Writing a PNG Decoder in Whiley!

Over the last few days, I have been writing GIF and PNG decoders in Whiley.  These form part of an image manipulation benchmark which I’m planning to use for experimenting with the compiler.  The PNG decoder, in particular, was rather interesting.  My implementation is based directly off the PNG Specification, ISO/IEC 15948:2003 (E). The PNG . . . → Read More: Writing a PNG Decoder 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)

Parallel Sum in Whiley

Recently, I’ve been working on a variety of sequential and concurrent micro benchmarks for testing Whiley’s performance.  An interesting and relatively simple example, is the parallel sum.  The idea is to sum a large list of integers whilst performing as much work as possible in parallel.

To implement the parallel sum, I divide the . . . → Read More: Parallel Sum in Whiley

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