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 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

Whiley v0.3.18 Released!

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 being made (although it is flushing out a lot of issues).

ChangeLog Lots . . . → Read More: Whiley v0.3.18 Released!

Whiley Features in the Dominion Post!

Today’s edition of the Dominion Post (Wellington’s Local Newspaper) features a nice article on Whiley:

Obviously, I’m very excited to see Whiley being talked about in our local newspaper, and I think the article does a nice job of it.  There is also an electronic version as . . . → Read More: Whiley Features in the Dominion Post!