Property Syntax in Whiley

Recently, I gave a demo which showed off thew new “Property Syntax” in Whiley. Whilst this is still in the devel branch it will make its way, soon enough, into the next release.

Understanding Effective Unions in Whiley

The concept of effective union types in Whiley exposes some interesting features worth considering. In particular, they result in a separation between the readable and writeable view of a type. But, we’re getting ahead of ourselves!

Program Specification in Practice?

Recently, as part of our Programming Languages Reading group, we looked at the paper “Contracts in Practice” by Estler et al., (see here for a copy). This is quite an interesting paper and the authors perform an empirical investigation as to how contracts are used by programmers in practice.

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

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.