In this post, we’re going to consider representing the classic C string in Whiley. This turns out to be useful as we can then try to verify properties about functions which operate on C strings (e.g. strlen(), strcpy(), etc). If you’re not familiar with C strings, then the main points are:
Roughly speaking, C . . . → Read More: Encoding C Strings in Whiley
A couple of weeks back, I gave a presentation to the Wellington Java User Group. The talk provides a useful introduction to verifying software in Whiley, and shows a bunch of interesting examples. Anyway, you can see the presentation here:
Wellington Java User Group Presentation from John Hurst on Vimeo.
. . . → Read More: Verifying Software with Whiley
Recently, I was listening to the latest edition of the Illegal Argument podcast, and it turns out they were discussing Whiley! (about 103:16 minutes in). The discussion was about how verification interacts with data from an untrusted source (e.g. from a database, network connection, etc). In particular, whether or not we can safely feed . . . → Read More: Verification with Data from Untrusted Sources
Recently, I created a Whiley Cheat Sheet for use in our SWEN224 course and I thought it was useful enough to share! The goal of the cheat sheet is to provide some simple examples to help you get going, rather than provide a comprehensive reference. I tried to cram as much as I could . . . → Read More: Introducing the Whiley Cheat Sheet!
In this article, I’ll look at some interesting issues relating to the use of break statements within loops, and how this affects the idea of a loop invariant. For some general background on writing loop invariants in Whiley, see my previous post. To recap the main points, here’s a simple function which requires a . . . → Read More: Loop invariants and Break Statements
As the Whiley system is taking better shape every day, I’m starting to play around more and discover things. In particular, there are some surprising issues surrounding while loops and their loop invariants. These are things which I’ll need to work on in the future if Whiley is to stand any chance of being . . . → Read More: Thoughts on Writing Loop Invariants
An important component of the Whiley language is the use of recursive data types. Whilst these are similar to the algebraic data types found in languages like Haskell, they are also more powerful since Whiley employs a structural type system. So, what does all this mean? Well, let’s look at an example:
define IntList as . . . → Read More: Iso-Recursive versus Equi-Recursive Types
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:
define nat as int where $ >= 0 define pos as int where $ > 0 define . . . → Read More: Compile-Time Verification and I/O
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. Consider these two different versions of a function f(any):
int f(any x): if x is string: return g(x) else: return . . . → Read More: Whiley Puzzler #1
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 (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