Articles

  • No categories

Reference Lifetimes in Whiley

The concept of lifetimes was pioneered in the Rust programming language, and builds on earlier notions of regions and ownership types. Lifetimes are considered one of Rust’s “most unique and compelling features”.

Recently, the concept of reference lifetimes has been added to Whiley by Sebastian Schweizer (@SebastianS90). In this post, I’m going to try . . . → Read More: Reference Lifetimes in Whiley

Whiley v0.3.40 Released!

The next version of Whiley is upon us, and this one includes a bumper package of changes.  In particular, I am very excited by the introduction of reference lifetimes into Whiley.

ChangeList Reference Lifetimes (#642).  This represents a fairly significant step forward in the evolution of the Whiley language.  Reference lifetimes have been implemented . . . → Read More: Whiley v0.3.40 Released!

Contractive and Uninhabited Types in Whiley

An interesting feature of Whiley is that it supports true recursive types.  These are surprisingly tricky to get right, and recently we came across some interesting examples that the Whiley compiler should (but doesn’t) check for.

Recursive Types

The following illustrates the syntax for recursive types in Whiley:

type Link is {any data, LinkedList . . . → Read More: Contractive and Uninhabited Types in Whiley

Whiley v0.3.39 Released!

Progress has slowed on Whiley now that Trimester 1 and my SWEN221 class with 220+ students has begun!  Despite this, development continues with more contributions from others which is great.  This release is largely a “cleaning up” and “bug fixing” release, rather than landing any big features.

ChangeList Parameterised Test cases (#580,#588).  Thanks to . . . → Read More: Whiley v0.3.39 Released!

Whiley v0.3.38 Released!

Finally, just over one month since the last release of Whiley, version v0.3.38 is released today! The list of changes is reasonably large and we should expect lots more going forward …

ChangeList Removed Tuple Types (#537).  Part of my ongoing work to simplify the language.  Tuple types were not heavily used in any . . . → Read More: Whiley v0.3.38 Released!

Whiley v0.3.37 Released!

Another big update to Whiley landed today, and includes a whole raft of changes. In particular, various algorithms in the automated theorem prover have been reworked to improve performance (though more still needs to be done here). A rough summary of the changes in this version is:

Performance Improvements for Automated Theorem Prover.  In . . . → Read More: Whiley v0.3.37 Released!

Encoding C Strings in Whiley

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

Verifying Software with 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

Introductory Lecture on Verification in Whiley

We’ve started using Whiley again in my second year course Formal Foundations of Programming. The aim of this course is to introduce students into a range of techniques related to software correctness. So far, we’ve looked at some static analysis and model checking tools.

Anyway, last week I gave an introductory lecture on writing . . . → Read More: Introductory Lecture on Verification in Whiley

Whiley v0.3.36 Released!

The next version of Whiley is upon us.  Whilst predictably late, this release packs quite a punch and contains a range of changes to the language syntax, and critical updates to the verifier.  Certainly, this version is capable of verifying more programs than any previous version.  The summary of changes includes:

Update list to . . . → Read More: Whiley v0.3.36 Released!