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
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):
int f(any x): if x is string: return g(x) else: return . . . → Read More: Whiley Puzzler #1
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!
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!