Verification Condition Generation with the Dijkstra State Monad

The Hoare state monad provides a powerful means of structuring the verification of higher-order, stateful programs. This paper defines a new variant of the Hoare state monad, which, rather than being a triple of a pre-condition, a return type, and a post-condition, is a pair of a return type and a predicate transformer. We dub this monad the «Dijkstra state monad».

Using the Dijkstra state monad, we define a new unification-based type inference algorithm, which succeeds in computing verification conditions for higher-order stateful programs. We prove our algorithm sound. We also prove it complete with respect to a simple surface-level typing judgment, resembling ML type inference. In other words, we show that any recursion-free program typeable in our surface system can also be typed in the Dijkstra monad. Thus, programmers may use our algorithm to type their programs in the Dijkstra monad and obtain more precise types, knowing that when our algorithm fails to infer a type, the failure is due to a typing error that can be detected by our simple surface type system. Recursive functions can be typed as usual if they are annotated with their loop invariants. We also show how to structure specifications so that despite the use of higher-order logic in the types of higher-order functions, we can generate first-order verification conditions for many programs. The result is a light-weight, yet powerful system for specification and verification of deep properties of stateful functional programs.

We have implemented our inference algorithm as a front-end to the F* compiler and report on a preliminary evaluation of our tool on a collection of benchmarks.