Modular verification of global module invariants in object-oriented programs

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