The Whiley project began in 2009 in response to the "Verifying Compiler Grand Challenge" put forward by Tony Hoare in 2003.
[3] Primarily developed by David Pearce, Whiley is an open source project with contributions from a small community.
The idea of such a tool has a long history, but was strongly promoted in the early 2000s through Hoare's Verifying Compiler Grand Challenge.
The purpose of this challenge was to spur new efforts to develop a verifying compiler, roughly described as follows:[6] A verifying compiler uses mathematical and logical reasoning to check the correctness of the programs that it compiles.The primary purpose of such a tool is to improve software quality by ensuring a program meets a formal specification.
Whiley follows many attempts to develop such tools, including notable efforts such as SPARK/Ada, ESC/Java, Spec#, Dafny, Why3,[7] and Frama-C.
Most previous attempts to develop a verifying compiler focused on extending existing programming languages with constructs for writing specifications.
[8] In contrast, the Whiley language was designed from scratch in an effort to avoid common pitfalls and make verification more tractable.
However, unlike most programming languages the integer data type, int, is unbounded and does not correspond to a fixed-width representation such as 32-bit two's complement.
Whiley has no built-in support for concurrency and no formal memory model to determine how reading/writing to shared mutable state should be interpreted.
The function's postcondition is made of three ensures clauses, each of which describe different properties that must hold of the returned index.
For example, in the first ensures clause, the variable index is retyped from int|null to just int on the right-hand side of the implication operator (i.e. ==>).
However, the loop invariant is required to help the automated verifier using in the Whiley Compiler to prove this function meets its specification.
Another important milestone in the evolution of Whiley came in version v0.3.40 with the inclusion of reference lifetimes, developed by Sebastian Schweizer as part of his Master's Thesis at the University of Kaiserslautern.