Documentation

Articles

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 . . . → Read More: Whiley v0.3.0 Released!

Whiley v0.2.9 Released!

Well, here’s version 0.2.9.   This includes numerous bug fixes, and several major feature updates:

Support for recursive algebraic datatypes Improved support for type testing, particularly of recursive types Syntax of function declarations has changed slightly to use where instead of requires + ensures.  See this post for more on why.

However, there remains a . . . → Read More: Whiley v0.2.9 Released!

Whiley v0.2.7 Released!

Well, finally, after a lot of effort I have a new release of the Whiley Development Kit.  To get it, follow the download links on the left.

The major difference over the previous version is that the theorem prover has been almost completely rewritten.  So, while on the surface it might not appear much . . . → Read More: Whiley v0.2.7 Released!

An Overview of Whiley’s Testing Framework

Testing that the Whiley-to-Java Compiler (wyjc) functions correctly is something of a challenge.  We must, as usual, check that the correct (JVM) code is generated, and that the type checker is accepting/rejecting the right programs.  However, we must also test that the theorem prover wyone is accepting / rejecting the right programs as well.  . . . → Read More: An Overview of Whiley’s Testing Framework

Whiley Compiler Status Update

So, a little update regarding the status of the Whiley compiler. I have spent a considerable amount of time redesigning the theorem prover over the last 8-12 weeks, and still haven’t managed to put everything back together. The reason for this was simply that I reached a brick wall in terms of the original . . . → Read More: Whiley Compiler Status Update