coma, an Intermediate Verification Language with Explicit Abstraction Barriers

We introduce coma, a formally defined intermediate verification language. Specification annotations in coma take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every call site, from the “implementation” part, which is verified only once, at the definition site. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths. We define a verification condition generator for coma and prove its correctness. For programs where specification is given in a traditional way, with abstraction barriers at the function entries and exits, our verification conditions are similar to the ones produced by a classical weakest-precondition calculus. For programs where abstraction barriers are placed in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. In addition, our procedure can factorize selected subgoals on the fly, which leads to more compact verification conditions. We illustrate the use of coma on two non-trivial examples, which have been formalized and verified using our implementation: a second-order regular expression engine and a sorting algorithm written in unstructured assembly code.