Whiley v0.3.0 Released!

Well, after a significant amount of effort, many sleepless nights, and too many test cases going green, then red, then green, then red … it’s finally here!!!

In the process of moving from v0.2.X to v0.3.0, I have rewritten probably 75% of the code from scratch.  The new version is working quite well, and there are lots of new features.  However, it remains some considerable distance from my goal of a system that could really be used in practice.

ChangeLog

There are so many changes, I can’t even remember half of them!  But, the main ones are:

• The compiler has moved to using an intermediate language called wyil.  This has simplified many aspects of the compiler, and made comprehending the system much easier.  Probably the strangest aspect of wyil, is how it encodes logic using a simple imperative, unstructured IL — but it works beautifully.
• Whiley has regained the while loop and also a for loop.  You can read more about that here.
• Whiley has moved away from a declared-type model, in favour of a flow-sensitive typing model.  You can read more about that here.  Overall, I think this has proven very effective.
• Whiley has gained anonymous tuples, and the syntax for records has been brought in line with [[JavaScript]].
• Whiley has gained the null value + type, which is particularly useful for terminating recursive types (see this page for an example).
• The command-line interface for influencing the compilation process has been redesigned, and is more flexible.  This still needs to be properly completed, but it is already proving invaluable (for debugging).
• I decided to revert my previous idea of using where instead of requires and ensures for pre- and post-conditions (which was introduced here).  Ultimately, using where had too many problems and it wasn’t very easy to understand.
• The number of end-end test cases has increased to 705 (+ a range of other unit tests)
• I have constructed a non-trivial benchmark, called Calculator.  This is a simple expression-tree calculator for parsing and evaluating expressions of the form e.g. “1+2*3”.  Unfortunately, this does not yet work with verification enabled.  You need to supply the command-line argument “-Nvc” to compile this.

Known Issues

There are a lot of known issues at the moment (most of which are related to the theorem prover).  However, some important ones I know are:

• There are some problems with type testing constrained union types.  The way that type tests are translated into Java Bytecode means, in some unsual cases, things will not work.
• Set comprehensions don’t work very well with verification enabled.  The real problem is that they now translate down into wyil for loops, and I need to generate [[loop invariants]] for them.  This turns out to be a real challenge for multi-variable comprehensions, and I hadn’t realised that until just now.  So, I’m going to ignore them for the moment, since you can also just write a for loop and give the loop invariant yourself.
• There awkwards issues with loop invariants and records.  More specifically, if you only modify one field of a record in a loop, the entire variable is marked as modified — meaning you lose knowledge that the other fields remain unchanged.

For the Future

Recently, I have been reflecting on the interaction between the compiler-proper and the SMT solver, wyone.  There is a lot of redundancy here and, more importantly, the verification process leads to completely incomprehensible verification conditions (at least, for non-trivial exampls).  This is starting to cause me some real problems, as I’m reaching the point where want some non-trivial examples to work.  But, debugging them is all-but-impossible.  So, I’m considering a move away from the style of generating verification conditions, in favour of a process that works directly on the wyil intermediate language.  Ultimately, the way this would work would be roughly equivalent to the way the SMT solver works; except that there would be no verification conditions and, instead, we would have individual execution paths through the function in question.  This should be easier to debug, for one thing, and also elminate significant reduncancy, for another.