The concept of class invariant in object-oriented programming

What is it about?

The only indisputable way to guarantee that programs function correctly is to prove their correctness the way we prove a mathematical theorem, with the additional condition that such proofs will be mechanically checked by computer tools. The technology for proving programs correct has progressed considerably, but practical obstacles remain to making it mainstream. One of them is the need, for object-oriented programs (the dominant technology in today’s IT scene), to specify the properties of objects through formal constraints known as class invariants. The basic concept of class invariant is simple: an invariant is simply a property connecting the components of a valid object. For example, in an account object, credits minus debits equals balance; in a person object, current date minus birthdate equals age; with two objects representing a person and a house the occupant of the residence of person p is p itself and the residence of the occupant of house h is h itself. Any programmer (and many non-programmers) can understand and apply the idea. Unfortunately, the class invariant concept, when applied to large-scale object-oriented programs, involves some nasty details which previous work has not addressed in a satisfactory way. The present article introduces a simple and coherent framework, theoretical and practical, for using class invariants effectively. It provides a novel classification of the obstacles, in three parts; then it develops a basic model in which these obstacles arise; then it removes them one by one to yield a sound and general version of the proof rule. It applies the rule to a number of examples, including tricky ones that have defied previous verification attempts. Such attempts have generally involved the need for programmers to add numerous annotations to the program, making their task much harder and requiring mathematical knowledge that few practicing programmers possess. The articles’ approach is intended to make life easy for programmers by not requiring higher-level mathematical abilities and avoiding any extra programmer annotation.

Featured Image

Photo by John Schnobrich on Unsplash

Photo by John Schnobrich on Unsplash

Why is it important?

All processes in today’s society rely on the proper functioning of software systems. Formal software verification using machine-checked proofs makes it possible in principle to guarantee this correct behavior, but practical roadblocks have prevented the spread of formal verification in the industry. The main challenge is to let programmers write their programs as they would otherwise, without undue extra baggage to enable verification, in particular without an undue need for extra program annotations (in addition to the code and basic specification elements). In the quest to simplify the task of programmers who want their program to be released with an unimpeachable guarantee of correctness, this article represents a significant step forward: it enables programmers to write class invariants — a major stumbling block until now — in a simple way, letting the underlying theory and tools take care of the difficult details.

Perspectives