Specification and Verification of Invariants by Exploiting Layers in OO Designs
Ronald Middelkoop, Cornelis Huizing, Ruurd Kuiper, E.J. Luit · TU/e Research Portal · 2008
The layering that is present in many OO designs is not accounted for in current interpretations of invariants. We propose to make layers explicit in specifications and introduce a new interpretation of invariants that exploits these layers. Furthermore, we present a sound, modular technique to statically verify that programs satisfy the new interpretation.