Specification and Verification of Invariants by Exploiting Layers in OO Designs

Abstract. 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.

• Type: Journal
• Year: 2008
• Where: FUIN
• Authors: Ronald Middelkoop, Cornelis Huizing, Ruurd Kuiper, Erik J. Luit
• Keywords: Current Interpretations, FUIN 2008, Layering, OO Designs