As the Whiley compiler continues to evolve, certain aspects of its architecture are really starting to mature. One of the more recent pieces to take shape is the verification pipeline. This is the process by which a Whiley file is converted into a series of verification conditions, which are then checked by the automated . . . → Read More: The Architecture of Verification in Whiley
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
In this article, I’ll look at a common problem one encounters when verifying programs: namely, writing loop invariants. In short, a loop invariant is a property of the loop which:
holds on entry to the loop; holds after the loop body is executed; holds when the loop finishes.
Loop invariants can be tricky to . . . → Read More: Understanding Loop Invariants in Whiley
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
With the latest release of Whiley, compile-time checking of constraints can be enabled with a command-line switch. So, I thought a few examples of this were in order.
Example: Absolute of an Integer
Consider this simple program:
define nat as int where $ >= 0 nat abs(int x): return x
This defines a type . . . → Read More: Illustrating Compile-Time Verification in Whiley
Whiley uses a flow-sensitive type system, and a verification engine to enable [[Extended static checking]]. My desire in designing these two subsystems is to keep them completely isolated. In particular, such that we can always compile and run a Whiley program with verification turned off. This requirement stems from the fact that verification of . . . → Read More: A Problem on Typing vs Verification