We present a novel technique for the verification of invariants
in the setting of a Java-like language including static fields and methods. The technique is a generalisation of the existing
Visibility Technique of Mueller et al., which employs universe types.
In order to cater for mutable static fields, we extend this topology to
multiple trees (a forest), where each tree is rooted in a class. This allows classes to naturally own object instances as their static fields.We describe how to extend the Visibility Technique to this topology, incorporating extra flexibility for the treatment of static methods.
We encounter a potential source of callbacks not present in the original
technique, and show how to overcome this using an effects system. To
allow flexible and modular verification, we refine our topology with a
hierarchy of `levels'
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.