Building verification condition generators by compositional extensions

This paper describes a technique that combines algebraic datatypes and monads to build derivative verification condition generators (VCGs) by extending a base VCG. Extensions are compositional and can be stacked while the base VCG is left unchanged. The technique can be used to build a set of weaker VCGs to do light weight verification. Moreover, it enables us to add an ability to generate validation traces. The paper explains the technique through an example that extends a simple language L₀ with new constructs to handle exceptions. To deal with exceptions, not only the logic of L₀ has to be extended with new rules, its structure also needs to be changed. We show that using our technique the extension can be implemented in a simple and compositional way, without any change to the underlying logic.