Modular verification of global module invariants in object-oriented programs
OPEN ACCESS
Author / Producer
Date
2004
Publication Type
Report
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Modules and objects both contain variables whose values may be constrained by invariants. For example, in the object-oriented languages Java and C#, a module is a class and its static fields, and an object is an instance of a class and its instance variables. The invariants of modules work differently both from the invariants of objects alone and from the invariants of modules in a procedural language. This paper presents a methodology for module invariants in an objectoriented setting. The methodology is sound, prescribes an initialization order of a program’s modules, supports the dynamic loading of modules and classes, and is amenable to static, modular checking.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
459
Pages / Article No.
Publisher
ETH Zurich, Department of Computer Science
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science