Modular Verification of Static Class Invariants

摘要: Object invariants describe the consistency of object-oriented data structures and are central to reasoning about correctness software. But object not only conditions on which a program may depend. The in programs consists just fields, but also static hold that is shared among objects. fields described by class invariants, enforced at level. Static can mention instance describing dynamic rooted fields. Sometimes there even relate many or all objects class; these relations, too, since they cannot be any one isolation. This paper presents systematic way (a methodology) for specifying verifying programs. methodology supports three major uses Java library. amenable static, modular verification sound.