Detail

Class invariants: old concept and new results

Class invariants play a central role in understanding object-oriented programming. They also raise some tricky problems for the verification of OO programs, in particular “furtive access”, resulting from callbacks, and “reference leak”, a consequence of aliasing.

I will start with a tutorial on class invariants, explaining why OO programmers should understand the concept (although today many do not even know that it exists). Then I will describe the verification issues, which have attracted a considerable amount of research, and present my own recent results which, I hope, provide the solution. They take the form of three rules: the O-rule, a general Hoare-style inference rule for object-oriented programming (surprisingly, until now no widely accepted rule exists); the export consistency rule, a simple sanity condition complementing standard information-hiding properties; and the inhibition rule, taking care of reference leak. The talk includes several examples, such as the Observer pattern and linked structures, which have proved difficult to handle in previous approaches, and shows how the rules handle them. A distinctive property of the approach is that it uses no new language construct and no new programmer annotations whatsoever.

The talk explains all the concepts it uses; it is accessible to anyone with basic experience of object-oriented programming.