Whiley Compiler (WyC)

Recently, I was lucky enough to meet Rustan Leino whilst at a conference in Tallin, Estonia.  The Whiley project owes a lot to Rustan, as much of his work has been the inspiration behind Whiley.  In particular, his PhD thesis introduced the idea of ... [More] Extended Static Checking and he then worked on the seminal . . . → Read More: Exploring The Verification Corner [Less]

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 ... [More] where $ >= 0 nat abs(int x): return x This defines a type . . . → Read More: Illustrating Compile-Time Verification in Whiley [Less]

Finally the next release of Whiley is upon us!  There are a few useful improvements in this release.  In particular, compile-time verification of constraints is again functioning and can be enabled with a switch. ChangeLog Improved performance of the ... [More] Whiley Build System.  In particular, this no longer scans all files reachable from the current . . . → Read More: Whiley v0.3.15 Released! [Less]

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 ... [More] example would go something like this: int val; try { int tmp = f(); // cannot . . . → Read More: Variable Scoping for Try-Catch Blocks in Whiley [Less]

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 ... [More] as { int data, Tree left, Tree right } define Tree as null . . . → Read More: Termination of Flow Typing in Whiley [Less]

Recently, I’ve had the pleasure of working with Eclipse and trying to build a plugin.  On the whole, I have to confess, I find that Eclipse is an extremely well-designed and considered piece of software.  The biggest problem, I suppose, is that it is ... [More] designed for a wide variety of tasks and this means . . . → Read More: Are Checked Exceptions Always Caused by I/O? [Less]

I’ve just been watching the following talk over on InfoQ: Software Quality — You know it when you see it.  Thanks to Craig over at SoftViz for pointing me to it.  The talk is quite interesting, with the focus being primarily around using innovative ... [More] visualizations of software to gauge quality. But, that’s not what . . . → Read More: Test to Code Ratio [Less]

Finally, it’s time for yet another release.  The main change with this release has been a reworking of the compiler framework into a more serious build system called, unsurprisingly, the Whiley Builder System (wybs).  This has helped integration with ... [More] both Ant and Eclipse.  However, there remain a few aspects of it that need improvement, . . . → Read More: Whiley v0.3.14 Released! [Less]

It’s 8:30am on the 29th Februrary, 2012.  After a large number of complaints, ATM and Eftpos services are finally restored for the Commonwealth Bank of Australia (CBA).  See this, this and this for more details. Why is this interesting? Well, CBA is ... [More] denying it had anything to do with the leap year.  Just a . . . → Read More: Commonwealth Bank of Australia (CBA) denies problem with Leap Year? [Less]

I’ve recently finished Paul Allen’s excellent memoir entitled “Idea Man” and the recent biography of Steve Jobs by Walter Isaacson. Obviously, I didn’t read them at the same time … but one after there other! But, they were a fascinating read taken together, as they cover some of the same story from . . . → Read More: Jobs versus Allen