David J. Pearce (Blog)

Compile-Time Verification and I/O

Tuesday, April 9th, 2013

A surprisingly common question people ask me when I talk about compile-time checking of pre-/post-conditions and invariants is: how do you deal with I/O? To understand what the difficulty is, let’s consider a simple example in Whiley:

Whiley Puzzler

Monday, January 14th, 2013

I was having an interesting discussion with a colleague today about various aspects of Whiley, and we came up with an interesting bit of example code which is something of a puzzler.

Whiley Features in the Dominion Post!

Thursday, January 10th, 2013

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.

A Source File with 72KLOC!?

Tuesday, December 11th, 2012

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:

Generating Verification Conditions for Whiley

Tuesday, December 4th, 2012

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:

Comparing I/O in C with Java

Wednesday, November 28th, 2012

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 productive.

Formalising Flow Typing with Union, Intersection and Negation Types

Wednesday, October 31st, 2012

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 different points in a program.

Profiling Field Initialisation in Java

Sunday, September 30th, 2012

Recently, I attended the annual Conference on Runtime Verification (RV2012) and gave a talk entitled “Profiling Field Initialisation in Java” (the paper itself is here). This is the work of my PhD student, Stephen Nelson, and he should take all the credit for the gory details.

A Misconception of Functional Programming?

Thursday, September 6th, 2012

Recently, I came across an article entitled “Useful Pure Functional Programming” which talks about the advantages of functional programming. However, something struck me about the way the author thinks about functional programming:

Java versus C++ Performance

Monday, August 13th, 2012

Recently, I came across an interesting discussion of C++ versus Java performance over on Stack Exchange. There was also some good discussion of the article on Reddit which included a link to an interesting article from Google.

3
4
5
6
7