Specification and Verification of Invariants by Exploiting Layers in OO Designs

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Middelkoop, Ronald | Huizing, Cornelis | Kuiper, Ruurd | Luit, Erik J.

Affiliations: Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB Eindhoven, The Netherlands. r.middelkoop, c.huizing, r.kuiper, e.j.luit@tue.nl

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.

Journal: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 377-398, 2008