What Motivates Us?

Here’s an interesting video that I just came across (adapted from Dan Pink’s talk at the RSA), which is currently doing the rounds: The video is about what motivates people to do things and, in particular, whether or not giving people more money means they do a better job.  Definitely worth a look … . . . → Read More: What Motivates Us?

Example: Sum Over a Positive List

So, here’s the first Whiley programming example.  Obviously, it’s pretty simple as Whiley is not quite ready for big code just yet.  The idea is to compute the sum of a positive list which, of course, will give you a positive number.  We want Whiley to realise this and correct us if there’s a . . . → Read More: Example: Sum Over a Positive List

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!

The Trouble with Quantifier Instantiation in an SMT Solver? Triggers.

So, i’ve been recently working through the quantifier instantiation mechanism in wyone.  This is a tricky, yet important topic.  There’s been a lot of interesting research in this area as well (see further reading below for some examples), although I found the papers often hard work at times.

Anyway, the basic idea is pretty . . . → Read More: The Trouble with Quantifier Instantiation in an SMT Solver? Triggers.

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