After being stuck with an outdated Eclipse plugin for quite a while, I’ve finally released a new version of the Whiley Eclipse Plugin (Wyclipse). This uses the latest version of the Whiley Compiler (WyC), and fixes a whole host of problems with the previous version. Specifically:
Whiley Projects are Standalone. Previously, every Whiley project . . . → Read More: Eclipse Plugin v0.1.0 Released!
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
Today I was attending the Dafny tutorial given by Rustan Leino at SPLASH’13. I have to say that this was the highlight of the conference for me. In case you haven’t come across it before, Dafny is a programming language designed for software verification. It has a lot in common with . . . → Read More: The Dafny Tutorial at SPLASH’13
This is a slightly quicker release than usual, with only a few relatively minor fixes and refactorings, etc:
Factored JVM Bytecode library into a separate project, called Jasm Various bug fixes mostly related to verification. See here for the complete list.
I’ve also been working quite a lot on the Eclipse plugin, and will . . . → Read More: Whiley v0.3.21 Released!
Well, this release is about 2 months overdue, but it embodies a lot of work. The main changes are:
Bug fixes. I’ve closed around 36 issues, many of which were intricate little bugs. Improved the verifier. Perhaps what has taken most time is the considerable amount of work I’ve into improving the verifier. This . . . → Read More: Whiley v0.3.20 Released!
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 return null
Here, the type null|int is a union type . . . → Read More: Understanding why Union Types are useful
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
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 about how, for example, to handle millions and millions of concurrent connections and we . . . → Read More: Input / Output and the Object-Oriented Paradigm
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, is probably worse than the previous release! However, on the other hand, I have . . . → Read More: Whiley v0.3.19 Released!