Sound Invariant Checking Using Type Modifiers and Object Capabilities

TL;DR

This paper introduces a sound runtime invariant checking system leveraging type modifiers and object capabilities, ensuring class invariants hold during execution with improved usability and performance.

Contribution

It presents a novel approach that uses existing language features for sound invariant verification, reducing annotation burden and enhancing efficiency over prior methods.

Findings

Lower annotation requirements compared to Spec#

Significantly fewer runtime invariant checks than D and Eiffel

Supports mutation, dynamic dispatch, exceptions, and non-determinism soundly

Abstract

In this paper we use pre existing language support for type modifiers and object capabilities to enable a system for sound runtime verification of invariants. Our system guarantees that class invariants hold for all objects involved in execution. Invariants are specified simply as methods whose execution is statically guaranteed to be deterministic and not access any externally mutable state. We automatically call such invariant methods only when objects are created or the state they refer to may have been mutated. Our design restricts the range of expressible invariants but improves upon the usability and performance of our system compared to prior work. In addition, we soundly support mutation, dynamic dispatch, exceptions, and non determinism, while requiring only a modest amount of annotation. We present a case study showing that our system requires a lower annotation burden compared to Spec#, and performs orders of magnitude less runtime invariant checks compared to the widely used `visible state semantics' protocols of D, Eiffel. We also formalise our approach and prove that such pre existing type modifier and object capability support is sufficient to ensure its soundness.