|
|||||
|
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): Version 1: 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! |
 |
||||
|
Copyright © 2020 David J. Pearce - All Rights Reserved 54 queries. 0.331 seconds. |
|||||
