Whiley Compiler (WyC)

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!

Recently, I got hold of a Papilio One (which you can think of as the Arduino of FPGAs).  The Papilio board has a Xilinx Spartan 3 on board, which is plenty enough to get started learning about FPGAs.  Here’s what the board looks like: Now, it might look big above … . . . → Read More: Testing out my Papilio FPGA!

The Whiley programming language is about developing more reliable software and, of course, embedded systems is one of the biggest areas that could benefit. Obviously, then, we need an “embedded system” to test Whiley with, right?  At least, that’s ... [More] the thinking behind my recent endeavor to create an Arduino-based Robot. After some discussion with our workshop . . . → Read More: Building an Arduino Robot (for Testing Whiley) [Less]

Yesterday, I was looking at the stats on Ohloh for the Whiley project and noticed that my total line count for the project had increased from around 65KLOCto 143KLOC over a very short amount of time: Confused, I was pondering this for a while.  Then it struck me: I’d checked in . . . → Read More: A Source File with 72KLOC!?

Whilst it’s been over three months since the last release of Whiley, this latest release is chocked full of improvements!  I’ve closed around 60 issues in that time, and have completely reworked the theorem prover from scratch.  This means ... [More] compile-time checking of constraints is starting to work better — however, there remains quite a . . . → Read More: Whiley v0.3.17 Released! [Less]

Probably the most interesting aspect of the Whiley language is that it supports compile-time verification of preconditions, postconditions and other invariants.  There are two main aspects of how this works: Generation of Verification Conditions ... [More] (VCs) from the source code.  A verification condition is a logical expression which, if proved to be satisfiable, indicates an . . . → Read More: Generating Verification Conditions for Whiley [Less]

Recently, I was having a somewhat heated discussion with a friend about the Java I/O library (specificially java.io.*).  His position was that the library is unnecessarily cluttered and verbose, and that  I/O in C is much simpler and more ... [More] productive.  Whilst I agreed with some of that, I also argued that the Java I/O . . . → Read More: Comparing I/O in C with Java [Less]

Just yesterday, I came across the ohloh website for the first time and was surprised to find the Whiley project already listed there.  If you haven’t seen it before, Ohloh is a site that attempts to gather stats and other information on open source ... [More] projects such as: who the developers are, how many commits . . . → Read More: The Whiley Project on Ohloh [Less]

Yesterday I came across an interesting talk given by Rustan Leino at the University of Edinburgh in 2011.  Rustan takes an interesting look overview over the subject’s history, and then shows several tools in action (including Code Contracts and ... [More] Dafny): Anyway, Rustan has a long history in program verification now, and was heavily involved . . . → Read More: Rustan on Automatic Program Verification [Less]

The Whiley language takes an unusual approaching to static typing called flow typing.  This helps to give Whiley the look-and-feel of a dynamically typed language.  The key idea behind flow typing is to allow variables to have different types at ... [More] different points in a program.  For example, consider the following code written in a . . . → Read More: Formalising Flow Typing with Union, Intersection and Negation Types [Less]