Hybrid Types , Invariants , and Refinements For Imperative Objects

To control the complexity of large object-oriented systems, objects should communicate via precisely-specified interfaces. Static type checking catches many interface violations early in the development cycle, but decidability limitations preclude checking all desired properties statically. In contrast, dynamic checking supports expressive specifications but may miss errors on execution paths that are not tested. We present a hybrid approach for checking precise object specifications that reasons statically, where possible, but also dynamically, when necessary. This hybrid approach supports a rich specification language with features such as object invariants and refinement types.