Abstraction and Subsumption in Modular Verification of C Programs

Abstract

Representation predicates enable data abstraction in separation logic, but when the same concrete implementation may need to be abstracted in different ways, one needs a notion of subsumption. We demonstrate function-specification subtyping, analogous to subtyping, with a subsumption rule: if 𝜙 is a Open image in new window of 𝜓 , that is 𝜙<:𝜓 , then 𝑥:𝜙 implies 𝑥:𝜓 , meaning that any function satisfying specification 𝜙 can be used wherever a function satisfying 𝜓 is demanded. We extend previous notions of Hoare-logic sub-specification, which already included parameter adaption, to include framing (necessary for separation logic) and impredicative bifunctors (necessary for higher-order functions, i.e. function pointers). We show intersection specifications, with the expected relation to subtyping. We show how this enables compositional modular verification of the functional correctness of C programs, in Coq, with foundational machine-checked proofs of soundness.