Making the best of class invariants
COM2 Level 4
Executive Classroom, COM2-04-02 and via Zoom (Hybrid)
Abstract:
In object-oriented programming, objects and the corresponding classes are subject to consistency constraints: class invariants. The basic concept is simple, but the details are surprisingly tricky to sort out because of the power of object technology and in particular of references and aliasing. The 2016 $-50 million DAO hack was actually due to an undetected invariant violation. In recent years we have worked out a precise semantics for class invariants and the associated proof rule. The talk will present the concept of class invariant, the challenges it raises, the semantic model, the proof rule, and why it is sound. The main result is that we can prove classes correct (as part of the AutoProof verification environment) without any need for programmer annotations (ownership, subject-observer specifications) that have been thought necessary to impose until now. The approach is annotation free and verifies programs ?as is?. Beyond verification, well-understood invariants also help produce clearer and more reliable programs.
Biodata:
Bertrand Meyer is Provost and Professor of Software Engineering at Constructor University (ex-SIT) in Schaffhausen, Switzerland. He has recently published a book on the Handbook of Requirements and Business Analysis, Springer, 2022 https://se.ethz.ch/requirements