We integrate static and dynamic contract-based verification of stateful programs. Although contracts are useful to reason about programs, naive introduction of mutable references makes the reasoning difficult because state-dependent contracts that have been successfully checked can be invalidated by state mutation. The problem is more acute in manifest contract systems, in which contracts are part of static types, in that the naive introduction of assignments would break their important soundness properties.

We address this problem by designing a manifest contract system where specifications of pure code fragments are represented by refinement types and specifications of impure ones are by computational Hoare types—a variant of Nanevski et al’s Hoare types—which express pre- and postconditions of stateful computations in the same language as programs. To prevent troubles caused by abusing references in contracts, we introduce a region-based effect system, which allows contracts in refinement types and Hoare types to manipulate references as long as they are observationally pure and read-only, respectively. We show that our calculus has the same kind of soundness property as existing pure manifest calculi and, furthermore, stateful computations satisfy their postconditions if they terminate without dynamic contract violation.

Following Belo et al., static verification in this work is ``post facto'', that is, we define the manifest contract system so that all contracts are checked at run time, formalize what dynamic checks can be eliminated safely, and show that programs with and without such checks are contextually equivalent—intuitively, checks of contracts can be eliminated when their satisfaction is derived from other, already established contracts. We also apply the idea of post facto verification to region-based local reasoning, which shows that satisfaction of preconditions which do not refer to references mutated by a computation is preserved even after executing the computation.