The Concept of Class Invariant in Object-oriented Programming

Class invariants exist because the values, or “fields,” making up objects are not arbitrary but often constrained by consistency properties. In an object representing a company, assets equal equity plus liabilities (“accounting equation” [58]). Every operation must preserve this property: If it modifies (say) the equity, then it must update at least one of the other two fields to ensure that it holds again.

In object-oriented (OO) programming, which structures programs based on the types of their data, or classes, such a property will be part of the invariant for the corresponding COMPANY class, part of its contract [39, 40]. Each operation of the class must, in addition to satisfying its own contract—assuming its precondition on entry, ensuring its postcondition on exit—preserve the invariant, part of the contract of the class, which in effect is “and”-ed to both its pre- and postconditions. Verification of OO programs relies on these rules.

This basic idea is straightforward, captured by a Groucho Marx quip in a cult scene of A Night at the Opera [36]: “That’s in EVERY contract: it’s called a sanity clause.” The more respectable software name for the “sanity clause” is the concept of class invariant, leading to an Invariant Hypothesis (Section 2.2), which makes it possible to reason about programs manipulating data structures. Three phenomena, made possible by the constructs of actual programming languages, can invalidate the Invariant Hypothesis, seeming to justify Chico Marx’s final retort in the scene: “There ain’t no sanity clause.” They are as follows:

Restrictions on the programming language yield a “Simple Model” of computation (Section 3), with a simple proof rule guaranteeing the Invariant Hypothesis. These restrictions are not acceptable for realistic programming, but removing them can (Section 4) raise the risks just cited. To remove these risks, Sections 5 to 8 successively drop the restrictions, updating the proof rule to preserve the Invariant Hypothesis. The final rule is suitable for verifying actual, unrestricted OO programs and, we hope, restore the faith in a sanity clause.

This work builds on the rich literature on class invariants in the past half-century and particularly the past decade (Section 11). Two distinctive features are as follows:

Examples of annotations (in approaches reviewed in Section 11) include wrap/unwrap instructions to express that at a given point objects satisfy, or not, their invariants; and “ownership” type annotations to express that certain objects (such as a list element) can only be accessed through others (such as a list header). They help the verification tools but complicate the programmers’ task and can turn them away from verification. Transferring as much of the burden as possible from programmers to the tools, the intent of the present work, is part of a general effort to make verification part of a normal programming process.

Other contributions include the following:

Limitations are discussed in Section 12; in particular, the rule does not yet cover inheritance, which will be addressed in a follow-up, and the soundness proof has not yet been mechanized.

The main theoretical result of this work is a proof rule, whose final versions appear in Sections 8.1 to 8.3. The discussion starts from a simple version (reflecting the intuitive notion of invariant), which holds in the Simple Model but does not handle the three obstacles that arise in practice; it then refines it in subsequent sections to overcome these obstacles one after the other. The goal of this step-by-step approach is to let the reader understand the precise justification for all components of the rule and the subtleties of the concepts involved.

For the reader who would like to have a preview of the overall result, the key inference rule derived from this discussion is (Section 8.3)characterizing the semantics of a call x.r (a) to a routine r with body body \(_r\) and formal arguments f. Pre \(_r\) and Post \(_r\) , applicable to both f and the call’s actual arguments a, are r’s pre- and postconditions. INV denotes the invariant of respective classes (client and supplier); it can be applied to specific objects, as in x.INV. INV_LOC is the part of INV that only depends on an object’s fields, not on other objects. Finally, INV / r is the result of “slicing” an invariant by a routine: removing all clauses of INV that have more visibility, in the sense of information hiding, than r. (Section 7 will introduce a small optional optimization allowing slightly more liberal versions of the conditions INV / r and a.INV / r.)

This rule has variants and complements (for initialization, for pure queries) but is the basis for proofs of the literature’s “challenge problems” in Section 10.

Presentations of object-oriented programming vary in their terminology, often influenced by a specific programming language. The present article uses the following consistent terminology, going back to Reference [38]:

We distinguish between the “class invariant,” a consistency constraint defined in a class text, applying to all instances of the class, and an “object invariant,” its application to a given instance. (For no apparent reason, some work cited in Section 11 uses “object invariant” to mean “class invariant,” even though the latter term has been around for 50 years.) Note that a class invariant, and corresponding object invariants for instances, denote a property of the fields of a single object, even though some of these fields can be references to other objects and the invariant may involve queries on them. A property that describes the combined consistency of several objects is called a multi-object invariant.

A runtime object structure is made of objects with mutual references and is called a heap. Figure 1 shows an illustration of a small part of a possible heap. Objects are, as noted, made of “fields.” Some fields, such as age, are basic values such as integers and strings, while others, such as spouse, are references to other objects. We say that such an object is attached to the reference as represented in the program; for example, the bottom object in Figure 1 is attached to the city field of the top-left object. The objects in the figure represent three persons and one city; some fields have been left blank.

A “qualified call” x.r (a) executes a routine r on a target object denoted by x, with (optional) arguments a. We may view the life of a single object S during execution as a sequence of such calls, illustrated by Figure 2. After an initial creation, through a “constructor” or “creation procedure” called make in the figure, the object executes successive operations (q, r, t) as a result of qualified calls from client objects (which will appear in a more complete version of the figure, Figure 3 in Section 2.8). Figure 2 shows the successive states (S \(_1\) , S \(_2\) , S \(_3\) , ...) of the object: after creation (make) and then before and after every qualified call (to routines q, r, t, ...).Every object is (Section 1.4) an instance of a class defined in the program text. The objects in Figure 1 are assumed to be instances of classes PERSON and CITY. Such classes typically specify consistency constraints on their instances, which make up the class invariant. For example (Section 1.1), the invariant of a COMPANY class may specify assets = equity + liabilities. In Figure 1, the invariant of class PERSON may include city = spouse.city (I live in the same city as my spouse) and spouse.spouse = Current (the spouse of my spouse is myself, with Current denoting the current object as explained below).

Invariants such as the ones cited are crucial for reasoning about programs. In spite of the name, a class invariant does not need to hold at all times; it can be temporarily violated during a routine’s execution, as at the marked point in r’s execution in Figure 2. But it must hold in states (S \(_1\) , etc.) where client objects can start a new call. An object that satisfies its invariant is said to be consistent.

This fundamental property is the “Invariant Hypothesis”:(“Initial” because a slightly revised version will appear in Section 6.5.) The “target” in x.r (a) is the object denoted by x. A “consistent” object satisfies the invariant of its class. The Invariant Hypothesis enables both program construction and verification to rely on the class invariant, by assuming that every object satisfies it whenever it is accessible from the rest of the system (in states S \(_1\) , S \(_2\) ...). We deduce this property simply by showing that every creation procedure (constructor) of the class ensures it (in state S \(_1\) in Figure 2) and every exported feature (every feature r that clients can use, in calls of the form x.r (a)) preserves it.

This mode of reasoning takes after mathematical induction (of which invariants, whether for classes or loops, are the application to computing). To deduce a property P of all natural numbers it suffices to prove that \(P (0)\) holds and that \(P (n + 1)\) follows from \(P (n)\) for any n. Then we can assert, for example, \(P (386)\) . We do not need to go back to \(P (385)\) , then \(P (384)\) , and so on.

To understand the importance of the Hypothesis, one may consider what happens if it does not hold. The invariant would just be a clause repeated explicitly in the pre- and postconditions of every routine, which would be expressed as Pre \(\ \wedge \\)\) INV and Post \(\ \wedge \\)\) INV, where INV captures common elements. But then every caller would have to establish x.INV before every call x.r (a). We call this transfer of responsibility from a class to its clients the Scandalous Obligation.

The Scandalous Obligation would render the notion of invariant largely useless (it is the equivalent of forcing the proof of \(P (386)\) to go over all previous values). Also note that the invariant may include secret (private) features, which clients cannot directly affect. The rest of this article shows how to ensure the Invariant Hypothesis, which unleashes the induction-like power of the invariant concept by enabling clients always to assume, prior to a call, that the supplier object is consistent (satisfies its invariant). A model for OO computation, such as those appearing in Sections 3 to 8, will only be considered sound if it guarantees the Hypothesis.

An issue that does not arise with mathematical induction is that the Invariant Hypothesis only talks about the start of qualified calls: What about their end? As Figure 2 suggests, nothing happens to an object between the end of a qualified call of target S and the start of the next call on S, but something could happen to other objects that invalidates S’s invariant (reference leak, studied in Section 8). Separately from the Invariant Hypothesis, the postconditions of all rules will ensure that objects are consistent on call completion too.

We now turn to a formal expression of these concepts.

Axiomatic reasoning on programs uses “Hoare-style” inference rules such as this one for non-OO routine calls (ignoring recursion and termination) [26],Such a rule is a proof technique: Below the line appears a property of a construct, here the call r (a); the rule states that we may deduce it by proving the property above the line, applicable to the body of r (f denoting its formal arguments). The properties involved are “Hoare triples” of the form {P} A {Q}, meaning that executing A in a state satisfying P will yield one satisfying Q.

Classic states that the effect of a call is that of executing the body after substituting actual for formal arguments. It captures the role of routines (methods): abstracting a computation by giving it a name and parameterizing it.

In an OO context, Classic remains applicable to unqualified calls r (a), executed on the current object (see 2.11). Also, if we ignore the invariant, to qualified calls:The No-Invariant rule is conceptually the same as Classic, but takes into account the role, in OO programming, of the target of a qualified call, here x, which it simply treats as if it were an extra argument.

The rest of the discussion will introduce variants of the rule No-Invariant. Since they have many elements in common, we can rely on a concise tabular notation to avoid repetitions and emphasize the distinctive novelty of each variant. This notation expresses No-Invariant as the highlighted part of the following table (the rest provides explanations, not repeated in later rules):Since the context is always the same, the notation further drops r (i.e., Pre stands for Pre \(_r\) and so on). On the supplier side, INV will stand for the invariant of class SC; on the client side, for the invariant of class CC. Since x is of type SC, x.INV stands for the invariant of SC applied to x.

No-Invariant does not recognize the role of the invariant; the author of the code would have to add it manually to Pre and Post for every exported routine r. Rule Pointless is a first attempt at integrating the invariant explicitly:(Multiple assertions in a box, such as INV and Pre in BS \(_1\) and BS \(_2\) , are to be combined by conjunction. In mnemonics for entries, BS \(_1\) , and so on, B stands for before and A for after, S for supplier and C for client.)

This rule and the ones that follow only talk about preservation of the invariant for an object that already satisfies it as a result of proper initialization. Section 9.1 will introduce a creation rule covering initialization.

The reason for calling the previous rule Pointless is that it fails to take advantage of the invariant. It is in fact the same as No-Invariant, with pre- and postconditions extended with the invariant.

The disappointment is clause BC, requiring clients to obtain x.INV prior to calls. This approach suffers from the Scandalous Obligation (2.2), losing the basic idea of invariants expressed by the Invariant Hypothesis. To satisfy the Hypothesis, we need a rule in which the invariant for the target object:

Under such assumptions, one may prove the correctness of any call, in the form

with no x.INV on the precondition side, simply by having proved once and for all, independently of any callers, the correctness of the routine, in the form

Proving a class correct means proving the IPP (plus initialization, see 9.1) for its exported routines, which then suffices (this is what the Invariant Hypothesis means) for proving the correctness of any call (CCP, without x.INV on the left).

Removing x.INV in BC gives an “ideal” rule, which satisfies the Invariant Hypothesis and in a simpler world would be the final word:(Since the Pre and Post parts are not specific to OO programming and apply equally to all rule variants, we omit them from now on.) The novelty is the highlighted empty BC entry, which does not contain the requirement x.INV on the caller. If the Ideal rule applies, then the callers to a routine satisfying the CCP:

The Ideal rule is the direct formal expression of the Invariant Hypothesis, and the formal embodiment of the notion of class invariant. (The antecedent of the rule—BS and AS—expresses the Invariant Preservation Property.) A “Simple Model” of computation, described in the following section, satisfies it. The vagaries of actual programming in realistic languages will threaten to bring back the Scandalous Obligation and require adjustments to the rule.

To understand how the Ideal rule applies and where it requires adaptation, one must put the lifecycle of a single object (Figure 2) in the broader context of an entire OO system’s execution, involving any number of objects (as in the heap of Figure 1). Figure 3 includes, along with the original supplier object S, the history—after initialization—of two of its client objects, C1 and C2.As in the earlier figure, S executes routines q, r...; Figure 3 shows that these executions result from qualified calls coming from clients C1 and C2. C1 calls q on S, and at some later time C2 calls r on S.

At any point during execution, one of the objects is the “current object,” known as Current (or “this” in languages such as Java). Each execution step is either

Execution starts with a “root” object, the first “current.” As a result of qualified calls, other objects become current. At any time, objects are partitioned into two categories (Figure 4): objects in the call chain, starting from the root down to ending with the current object, called active; all others, called inactive. (In concurrent programming, execution may include more than one root and more than one call chain.) Note that an object S is active if it has started and not yet completed a qualified call x.r (a). We call r the “routine of” the active object; r and other routines along the call chain are the “active routines.” Note that the current object is active, although the semantic rules will treat it differently from other active objects. Inactive objects appear in the lower part of Figure 4.

As suggested in that figure, fields of objects in any category may be references to objects of any other.

We saw in Section 2.2 that during execution some objects may temporarily become inconsistent (violate their invariants). The objects in Figure 3 go from consistent state to consistent state (blue squares), traversing inconsistent states in between. In particular, internal operations often break the invariant: with the invariant clause assets = equity + liabilities, after a change to equity the invariant no longer holds. The routine must restore it by changing one or both other fields.

The key formal property of an OO computational model is the specification, represented by a thick black rectangle in Figure 4, of which objects must be consistent. It will be known as a Global Consistency Property or GCP. Figure 4 illustrates version GCP-0, whose definition in Section 3.2 below will state that among non-current objects only active objects are permitted to be inconsistent. They include the current object, which in all models can be inconsistent, since it may be executing an internal operation. Later models with their associated proof rules, representing increasingly sophisticated forms of OO computation, use different variants, GCP-1 to GCP-3. For each variant, we will need to prove two results:

(A Global Consistency Property is a global invariant on the heap. To avoid confusion, the discussion will reserve “invariant” for class and object invariants.)

Along with qualified calls x.r (a), OO languages support unqualified calls r (a), which apply a routine r to the current object. To avoid any confusion (sometimes found in the literature), note that the rules on class invariants apply to qualified calls only. An unqualified call r (a) can be understood (“inlined”) as the sequence of instructions making up the body of r (accounting for possible recursion), and is not subject to the invariant: It may not assume it on entry and does not have to ensure it on exit. Accordingly, the applicable rule for such a call is the traditional non-OO call rule: Classic from Section 2.3, applied to the current object. What determines the rule to apply is not whether r is exported, but whether a given call is qualified, x.r (a), or unqualified, r (a). (Note that Current.r (a) and r (a), which perform the same computation, are bound by different rules: the first is subject to the invariant, the second is not.)

A routine r involved in an unqualified call can, of course, include a qualified call, but that call is only relevant for the process of proving r itself correct.

The Simple Model makes three assumptions:

A “callback,” “direct,” or “indirect” is a qualified call whose target is (respectively) the current object or another active object. (An illustration of an indirect callback will appear in Figure 8, Section 6.7.) Assumption SM1 rules out both kinds.

Assumption SM2, Invariant Preservation, expresses the invariant concept in its simplest form. It is guaranteed by the antecedent part of the Ideal rule (Section 2.7), BS and AS (Invariant Preservation Property as seen in Section 2.6).

SM3, Invariant Locality, excludes any invariant clause x.some_property where x is a reference to another object: the invariant depends on the fields of a single object. A clause such as assets = equity + liabilities, involving only integer fields, satisfies this condition, but not any of the example invariants on PERSON, such as spouse.spouse = Current, which involves another object. These examples indicate that the restriction is severe.

A formal OO framework consists of a programming language (with any associated restrictions), a computational model, and Hoare-style inference rules for qualified calls (and initialization as will be added in Section 9.1). We say that the framework is sound if the computational model satisfies the rules.

We will now prove that the Simple Model with the Ideal rule is sound.

The Simple Model’s key property is that it preserves Global Consistency, version GCP-0 (Section 2.10, see Figure 4): at all times, all inactive objects are consistent.

Global Consistency Lemma: in the Simple Model, all runtime events preserve GCP-0.

Proof: While specifying the full semantics of a program’s execution requires a formal model of the entire language, the analysis of invariant-related behavior need only consider runtime events of three kinds (recognizable in Figure 2):

The following table characterizes each in terms of (1) whether it affects which object is “current” and (2) whether it affects the invariant of any object.

Events of each kind preserve GCP-0:

This proof required all three assumptions SM1, SM2, and SM3 of the Simple Model. Subsequent sections will adapt it as we remove them one by one.

In passing, we have proved (discussion of G2 and G3) that the Simple Model satisfies the Consistent Target Theorem (CTT): On entry and exit of a qualified call, the target is consistent.

Simple Model Theorem: For the Simple Model, the Ideal rule is sound.

Proof: The property to establish is that if a routine has been proved correct (antecedent of the rule, with INV in both the pre- and postconditions of the routine, entries BS and AS), the postcondition x.INV (entry AC) will hold upon completion of any qualified call. This property immediately follows from the CTT theorem above, which also implies that the Invariant Hypothesis holds.

This result justifies leaving the BC entry blank in the rule: The client does not need to worry about x.INV before the call, avoiding the Scandalous Obligation.

An important observation applies to proofs of soundness for Ideal and its followers. All of them have the postconditions INV for the supplier (entry AS) and correspondingly x.INV for the client (AC). Unlike Pointless, however, they do not include the precondition x.INV for the client (entry BC); Ideal itself has nothing there. If we are able to prove the Invariant Hypothesis, then we guarantee that x.INV holds on start-of-call and hence can simply apply Pointless to derive the postcondition AC. As a result, to prove such a model sound it suffices to prove that its satisfies the Invariant Hypothesis.

A simple example, introduced in Reference [41], is subject to all three issues (other examples appear in Section 10). It involves a single class PERSON and a single routine of interest, marry. The class has attributes

where spouse is declared detachable as it can be a void (or “null”) reference. It has the following invariant:

expressing the relationship between the attributes. ( \(\Rightarrow\) denotes implication, and a name before a colon in an assertion clause, such as distinct, is a tag identifying the clause.) is_married could be a function (returning true if and only if spouse \(\ne \\)\) Void), but defining it as an attribute helps reveal potential problems.

Reference [41] analyzes the difficulty of writing a procedure marry (other: PERSON) that will result in setting the spouse field of the current object to other and its is_married field to True. The procedure has as a precondition that both the current object and other are unmarried. A straightforward recursive implementation, where marry calls other.marry (Current), will not work, because this call will violate the second precondition. The following variant avoids this problem:

The call other.spouse is, as marked, a callback. It finds the original object inconsistent, violating married_iff_has_spouse, since spouse is not Void but is_married is still False to satisfy the precondition. No reshuffling of instructions will (to our knowledge) satisfy both the preconditions and the invariant. All code is available in the article’s repository [3] for the reader to try out.

After callbacks, furtive access. In line with Reference [41] it is possible to write a non-recursive version with auxiliary routines:

both visible, for obvious reasons of information hiding, only to PERSON (that is, not usable from other classes). The callback goes away, but furtive access arises, in the form of violated invariants, for example if we write marry as follows (pre- and postconditions are as with the preceding version and omitted for brevity):

Before instruction 4, the clause married_iff_has_spouse of other’s object invariant does not hold, violating the Invariant Hypothesis. With the elementary semantics of invariants as suggested so far, such a violation will arise with any reordering of the four: As soon as one of instructions 2 and 4 has been executed, other will violate its clause married_iff_has_spouse (and executing the other one of these instructions would be the only way to restore it).

The invariant at issue here is not the invariant of the current object but the invariant of other. It is frustrating that these violations cause trouble, because they are all intuitively harmless: As in an internal (unqualified) call, the intermediate states of other can be inconsistent as long as the final one is consistent. In software verification, however, there is no simple equivalent of “trust me, I know what I am doing, everything will be fine in the end!”

Finally, reference leak. In the same example, assume that we somehow have obtained a solution for callbacks and furtive access and a suitable version of marry. A reference leak will occur, illustrated in Figure 5, if some code using references Alice, Bob, and Charles to distinct objects performs

where divorce simply sets is_married to false and spouse to Void (its code appears in Section 10.1). Calling divorce is necessary, because marry’s precondition. After these calls, Alice.spouse is Charles, but Bob.spouse is still Alice, so Bob.spouse.spouse is Charles, causing Bob to violate spouse.spouse = Current.

The code is intuitively buggy: divorce should reset the is_married and spouse fields of the previous spouse. But divorce satisfies its contract (with obvious pre- and postconditions), and in particular it preserves the class invariant for the target object, here Alice. The scary part is that one may break another object’s invariant, here Bob’s, without performing any operation on it. Any proof technique relying on a simple invariant concept (as in the Simple Model) will miss the bug as all routines satisfy their contracts.

Stating that the code is “buggy” means, more formally, that it violates the Invariant Hypothesis. The violation will only cause trouble, however, in the next qualified call, if any, of target Bob. This property is the crux of the reference leak problem: It does not immediately manifest itself but results in a corrupted data structure, with some sitting ducks—inconsistent objects—ready to fall prey to the next qualified call.

The rest of this article develops a sound proof rule addressing all three issues.

The basic observation is that prior to executing a qualified call an object must make itself amenable to callbacks, meaning that it should guarantee its invariant. Hence the next version of the rule:For clarity, occurrences of INV in the statement of this rule refers to the corresponding class: S for the supplier side, C for the client side. The new element, highlighted in BC, is INV \(_C\) . The use of C instead of S and of INV rather than x.INV is not a typo: We are talking of the invariant of the calling object. Compare with the presence in Pointless, at the same position BC, of x.INV, meaning x.INV \(_S\) , imposing a Scandalous Obligation on the caller. Here, by using INV \(_C\) , the object takes care of ensuring its invariant before starting a qualified call (like a person who cleans up the house before going out on a walk, just in case someone comes to visit during that time).

The requirement of wrapping up before a qualified call will be loosened in Section 6, and further in Section 7, which introduces a “smart” version of the invariant (removing the wrapping-up requirement if no callbacks may occur).

In some methodologies, as noted, ensuring the invariant before an outgoing call is the task of a special wrap instruction (Section 11). The Callbacks rule achieves the wrapping-up without imposing an annotation on programmers.

The computational model corresponding to rule Callbacks, which we call the Callback Model, uses a new version GCP-1 of Global Consistency.

Compared to GCP-0 from the Simple Model, GCP-1 restricts the set of objects that may violate their invariants, now limited to at most one object, the current object. Figure 6 (which drops inter-object references, not needed for the discussion) is the counterpart for GCP-1 to Figure 4 for GCP-0.The Global Consistency Lemma now states that all operations, assuming SM2 and SM3 (but no longer SM1, invariant preservation) preserve GCP-1. As before (Section 3.2), each step demonstrates this property for one of the three types of event:

In passing we have proved an extreme form of the GCP, the Quasi-Constant Consistency Theorem (QCCT-1): In the Callback Model, in all states other than immediately after an internal operation, all objects are consistent. (Steps G2 and G3 of the proof showed that consistency holds of all objects after start-of-call and end-of-call, and internal events are the only other case.)

QCCT-1 is the closest we will ever come to a literal reading of the word “invariant” as a property that always (in this case, almost always) holds.

To prove the soundness of the Callback model for rule Callbacks, it suffices (see Section 3.3) to note that it satisfies the Invariant Hypothesis. That property is part of QCCT-1: The target is consistent after start-of-call. (QCCT-1 also tells us that the target is consistent after end-of-call.)

One of the object-oriented principles is information hiding (introduced by Parnas [50] in the same year as the first article mentioning class invariants [27]), which lets each class define which of its features and other properties it makes available (“exports”) to others (its clients). Many OO languages offer ways to fine-tune this decision through selective export, whereby a class exports specific features to specific clients; examples are the “friends” mechanism of C++ and “internal” accessibility in C#. In Eiffel, one may declare a feature in a clause starting with feature {A, B, &} to specify that it is only exported (or “visible” per the terminology defined below in Section 6.3) to classes A, B, … and their descendants.

Previous work seems to have missed the relationship of selective exports to the furtive access problem of class-invariant semantics, and its potential role in solving the problem without requiring additional programmer annotations.

Observation of utility routines such as set_married and set_spouse and their counterparts in other furtive-access-prone code (such as the Observer pattern) reveals that in properly written code they are not publicly exported. Instead, they are selectively exported to the relevant class, in this case PERSON itself. As a consequence, while a call Alice.marry_stepwise (Bob) (Section 4.3) may appear in any class (since all versions of marry should be publicly exported), other.set_married is only permitted in class PERSON (and descendants).

Using information hiding criteria in the proof rule combines design principles and correctness concerns. The reasoning is that a routine should not have to account for invariant clauses of visibility higher than its own. All three invariant clauses of PERSON involve public features, spouse and is_married, of higher availability than set_spouse and set_married; they should not have to preserve these clauses. The situation with examples such as Observer is similar.

As a reminder, an invariant is made of a sequence of clauses; the one for PERSON (Section 4.1) has three clauses (here without tags): spouse \(\ne\) Current, is_married = (spouse \(\ne\) Void) and is_married \(\Rightarrow\) (spouse.spouse = Current). The invariant is understood as the sequential conjunction (“and then”) of these clauses.

Regardless of the language mechanism for selective exports, the visibility V (r)of a feature r of a class C is defined as the set of classes that may use r as clients, in qualified calls x.r (a) with x of type C. The example has assumed so far (Section 4) that the features of class PERSON have full visibility (they are exported to all classes) except for two of them, exported only to class PERSON itself: V (set_married) = V (set_spouse) = {PERSON}. Visibility gives a preorder relation (reflexive and transitive) on the features of a class: we write r \(\le\) g to express that V (r) \(\subseteq\) V (g) (g is exported to the same classes as r, and possibly to some additional ones).

The queries of an invariant clause are the queries that appear in it either by themselves or as targets of calls. For example, the queries of

a and b.c

are a and b (but not c, which is the feature of a qualified call, not a feature of the invariant expression itself).

Visibility, defined above for individual features, also applies to invariant clauses. The visibility V (CL)of an invariant clause CL is the intersection \(\cap\) V (q) of the visibilities of all its queries q. The preorder relation also follows: CL1 \(\le\) CL2 means that \(\cap\) V (q1) \(\subseteq\) \(\cap\) V (q2) for queries q1 of CL1 and q2 of CL2; in other words, for any class C to which all queries of CL1 is exported, all queries of CL2 are also exported to C. The preorder relation can similarly hold between invariant clauses and features: CL \(\le\) r means that V (CL) \(\subseteq\) V (r), that is to say, r is exported to all classes to which all queries of CL are exported.

Finally, if INV is the invariant of a class, then its slicing by a feature r of that class, written INV / r, is INV restricted to its clauses CL such that CL \(\le\) r. In other words, INV / r is the part of INV that has no more visibility than r.

The clauses of the invariant of class PERSON (repeated at the beginning of this subsection) all have spouse or is_married among their features, and hence have full visibility, since these features are public (exported to all classes). Since marry, in all its versions, is also public, INV / marry is the full INV. However, INV / set_spouse and INV / set_married are empty invariants, since the given features have lesser visibility (they are exported to PERSON only). In the examples summarized in Section 10, sliced invariants are in-between these extremes.

The following Slicing Implication Theorem holds: If r \(\le\) g, then INV / g \(\Rightarrow\) INV / r. Proof: for any clause CL of INV / r, CL \(\le\) r by the definition of slicing. Hence CL \(\le\) g, implying—again by the definition of slicing, applied now to INV / g—that CL is one of the clauses of INV / g. So all the clauses of INV / r are also clauses of INV / g. As a consequence, remembering that an invariant denotes the conjunction of its clauses, INV / g implies INV / r.

A caveat about slicing is that some invariant clauses may need reinforcing to remain defined. For example, a good prover will accept an invariant clause c involving 1 / y if earlier clauses state x = y and x > 0; slicing x off removes these clauses and makes c potentially undefined, hence useless for verification. It is the programmer’s responsibility to make sure that all invariant clauses are meaningful, pre- and post-slicing (here, precede c’s condition by y \(\ne\) 0 \(\Rightarrow\) ).

Active objects have been defined as the objects in the call chain (Figures 4 and 6). Each is executing “its call” to “its routine,” r, s, t in the figures. These routines can have arguments of reference types. The term extended-active objects will cover active objects plus those attached to arguments of calls in the call chain. (Remember that an object is “attached to” a reference if that reference points to it.) For brevity, “inactive” will from now on denote all non-extended-active objects (in the thick rectangle at the bottom of Figure 7). Note that the current object is active and hence extended-active, but all the properties below involving extended-active objects will be restricted to non-current ones.

As illustrated in Figure 7 and explained next, in the Slicing Model all non-current extended-active objects (those in the large dashed rectangle) will satisfy their invariants sliced by the routine of the respective call.

Consider a non-current extended-active object, with invariant INV. It either started the execution of a qualified call x.r (a) or is one of its arguments a. It is partially consistent if it satisfies INV / r: the invariant sliced by the current routine. Obviously, consistent implies partially consistent. A non-current object is relatively consistent if it is either consistent or partially consistent.

GCP-2, the new variant of the Global Consistency Property (Figure 7), differs only slightly from GCP-1 (compare to Figure 6): All non-current objects are relatively consistent. In particular, any (non-current) object in the call chain or attached to an argument is partially consistent (it satisfies INV / r for its routine r). All other non-current objects are fully consistent.

The Invariant Hypothesis (Section 2.2) similarly becomes the Relative Invariant Hypothesis, stating that at the start of any call, the target satisfies its relative invariant (its invariant sliced by the feature of the call).

Notation: L.INV, for a list L, is the conjunction of x.INV for all elements x of L (in the rule, L is a list of formal or actual arguments, f or a). Here is the rule:(We no longer need C and S subscripts for INV.) Notes on rule Sliced:

The soundness of the Sliced rule requires two conditions on programs, to be enforced by the programming language.

Export Consistency Condition: in any qualified call x.s (a) appearing in a routine r, s \(\le\) r.

In other words, a routine may only perform qualified calls to routines with the same visibility or less. In the example of Figure 8, visibility along the routine sequence p, q, t, r can only remain the same or decrease. This reasonableness rule (do not rise above your own rank) can be compared to the practice of Web browsers such as Firefox, which let users start a new public or private window from a public window, but, from a private window, only a private one.Under the Export Consistency Condition, the following Safe Indirect Callback Theorem holds: In an indirect callback of routine r, the routine q of the target has the same visibility as r. (See Figure 8.) Proof: from the Export Consistency Condition, r \(\le\) q and q \(\le\) r. (From Section 6.3, “ \(\le\) ” on features is only a preorder, but on the associated visibility sets such as V (r) the relation is antisymmetric, since it is simply “ \(\subseteq\) ”.)

The second language condition needed for the soundness of the Slicing Model is the Selective Export Call Rule: in a call x.r (a) where r is selectively (rather than fully) exported, the target x must be a formal argument of the enclosing routine. (In other words, x may not be an attribute or a local variable.) This restriction does not affect the actual power of the programming language, because it is always possible to wrap a call in a routine. Informal examination of code using selective exports shows that most selective-export calls are indeed on arguments and that only a small amount of tweaking may be needed, as in two of the challenge-problem examples, marriage (Section 4.1) and circular list (Section 10.2), whose verification led to introducing an extra argument.

The soundness of the Slicing Model also assumes that a routine cannot change the values of reference variables passed to it as actual arguments in a call. In other words, such arguments are passed by value. Many modern OO languages (such as Eiffel and Java) satisfy this common-sense condition, but others may violate it, requiring adaptations of the model presented here.

As with earlier rules, the core of the soundness proof for Sliced is the proof of the Global Consistency Lemma, here stating the preservation of GCP-2 (all objects except the current one are relatively consistent) through events of all three kinds:

Steps G2-A and G3-B involve an object that GCP-2 allows to be inconsistent, because it is current. It is in fact relatively consistent in both cases, yielding an updated form QCCT-2 of the Quasi-Constant Consistency Theorem: In the Slicing Model, in all states other than immediately after an internal operation, all objects are relatively consistent. Proof:

As a consequence of QCCT-2, the Slicing Model satisfies the Invariant Hypothesis and hence (see 3.3) is sound.

We need a precise definition of the notion of dependents of an object. At any time during execution, the dependent set of an object S, Dep (S), is the set of other objects C whose invariants have a clause x.some_property where x is a field of C attached to S. In Figure 5, for example, Dep (Alice) = {Bob, Charles}.

In reference to the program text, we may use Dep (x) to denote Dep (S) for the object S attached to x at runtime (empty if x is Void). If we could determine that set, then the corresponding Strong proof rule would be the same as Sliced with a clause on dependents added above and below (highlighted).Soundness: GCP-2 remains. So does the previous proof of soundness (Section 6.8), with Invariant Locality relaxed into “an object’s invariant only involves fields of the object itself and its dependents.”

In effect, the Strong rule addresses—rather than the classical notion of class invariant—the notion of multi-object invariant (Section 1.4) by extending the invariant of an object with the invariants of all its dependents. Implementing this rule into a verifying tool requires computing the Dep sets, which in the absence of programmer annotations implies an analysis that is global (on the entire program) rather than modular (class by class). As a conjecture, a modular implementation may be applicable to classes whose invariants satisfy specific patterns (see the “mirroring” suggestion in Section 11.14 of Reference [40]).

Weak-C (“C” for “Client” or “caller”) puts the burden on callers:This rule relies on splitting any invariant into two parts: INV_LOC and INV_REM, for “local” and “remote.” INV_REM contains the clauses that have a subexpression of the form b.some_property where b denotes a reference field. In PERSON (4.1), INV_LOC includes two of the three clauses distinct and married_iff_has_spouse; the third one, reciprocal: is_married \(\:\Rightarrow \:\) (spouse.spouse = Current), goes into INV_REM (because of spouse.spouse).

We say that an object is locally consistent if it satisfies the local part of its invariant. (Local consistency could also be partial in the sense of slicing as defined in Section 6.5, but will only be applied in the unsliced case.)

The weak variant is based on the observation that the Invariant Hypothesis would hold if the invariant consisted of INV_LOC only; the risk of reference leak comes from INV_REM, which GCP-2 does not allow us to assume on start-of-call. GCP-3, the new GCP, is (change from GCP-2 highlighted):

The inactive part of the heap (bottom part of Figure 7 and predecessors) consists of objects that are “just sitting there,” ready to serve as target of future calls. In GCP-2 and previous models, they were fully consistent, in anticipation of ensuring the Invariant Hypothesis in those calls. With GCP-3 this massive guarantee of consistency no longer holds: We must cope with the possible presence of inactive objects that are only locally consistent. Under Weak-C, callers can only rely on the local consistency of these objects, and must ensure the rest.

Soundness: The Invariant Hypothesis continues to hold for the local part of the invariant and for the remote part is ensured by the caller (entry BC \(_3\) ).

Rule Weak-C, by reintroducing a limited form of Scandalous Obligation (a partial return to Pointless of Section 2.5), makes the client responsible for invariant elements that could have been messed up by a “man in the middle” such as Bob in the marriage case. The next rule frees the client from the Scandalous Obligation by making life harder for the supplier instead.

In rules governing routine calls, we may always move an obligation from the client’s to the supplier’s precondition. Rule Weak-S (“S” for “Supplier”) transfers responsibility for the remote part of the invariant from the client (as in Weak-C) to the supplier. Removing INV_REM on one side means adding INV_LOC to the other, maintaining the Invariant Hypothesis and hence soundness: A criticism of this rule is that it hands over some of the responsibility from the verifier to the programmer. For each routine:

The approach is “lazy,” as noted, in that it may leave inconsistent objects around. This possibility causes no threat to program correctness, since subsequent operations on such an object will have to restore consistency. With the strong approach such a situation would not arise, but the price to pay is that operations on an object must also take care of updating other objects whose consistency depends on it.

While Strong remains a possible choice, Weak-S appears, in spite of the preceding objections, to be the best available rule for proving the correctness of object-oriented programs and the main result of the present work. It was given in the usual style of Hoare inference rules (without the abbreviations introduced in the last sections) in the Preview Section (1.3) and is used for the proofs of example programs in Section 10.

Weak-S and predecessors govern a qualified call x.r (a) where x denotes an existing object that, per the Invariant Hypothesis, satisfies the invariant (at least its local component). Such rules correspond to the induction step in a proof by induction. We also need an initialization rule, corresponding to the base step.

The initialization mechanism is part of object creation, variously written:

The goal of object creation is to obtain an object satisfying its invariant. In adapting the preceding rules, it suffices to remove any property of the object itself on the precondition side—INV for the supplier (BS) and x.INV for the client side (BC), which makes no sense for a creation instruction as it creates a new object from scratch. (Of course any specific precondition of the creation procedure is still applicable; remember that the tabular notation used, since Section 2.7 ignores such routine-specific pre- and postconditions, but they reappear in the rule when we express it in full, in the classical notation of Hoare logic used for example for Weak-S in 1.3.) The postcondition side remains, as well as the conditions on arguments. The creation variant of Weak-S, applicable to an instruction create x.make (a), is Weak-S-Creation:DEF \(_S\) denotes the property that fields of the new object have default values (typically zero for integers, etc.). Including DEF \(_S\) is appropriate for languages such as Eiffel, Java, and C#, which specify default initialization rules; for C++, which does not, the BS \(_1\) entry remains blank. Since in a creation instruction there is no prior “current”, the rule needs neither slicing nor (as a consequence) the “smart” versions of the invariants (Section 7): A just created object must always satisfy the full invariant.

A query is an operation returning information about an object. It can be an attribute, giving the value of a field of the object, or a function, returning the result of a computation on those fields.

It is common programming practice (violating the “Command-Query Separation” design principle, References [39, 40]) to let functions change objects. Then the above rules for procedures are applicable to functions, with postconditions extended by properties of function results. The question remains of pure queries, which cannot change the state, and include attributes and side-effect-free functions.

The postcondition side of previous rules, AS and AC, is irrelevant for a routine that cannot change any object. Pure-query rules correspondingly have only one column (BS and BC), the same as in the corresponding rules for procedures.

The results of this simplification (with no new elements, just a removal of the postcondition column in the general rules) are given here for the record:Applying these rules assumes that the verifier can ascertain that a query is pure, either through a language rule or by static analysis. Both approaches have received considerable attention but fall beyond the scope of the present work.

This discussion has assumed a sequential programming context. In an unbridled concurrent framework, for example using multithreading, there is no hope for a meaningful notion of class invariant, since furtive access is ever looming. The risk of an Ethereum-DAO-like failure is consequently high.

Preserving the notion of class invariant, and the associated reasoning capabilities, requires a more controlled concurrent mechanism. In SCOOP [18], all access to shared objects is exclusive; then the entire reasoning and rules of this article apply unchanged.

For expository purposes, this article has introduced the rules as successive versions. The final result, however, is precisely defined. The rules to be applied for verification are as follows:

The class text with contracts is the following (in the interest of space the formatting does not respect indentation rules, and the creation procedure is omitted):

(Routine divorce has an argument—which must equal to spouse—because of the Selective Export Call Rule (Section 6.7), but it is easy to wrap it into a routine with no argument, as done with insert_right in the next example.) The proof appears as (a), (b), and (c) below. For conciseness, such proofs use a tabular notation, with one row per goal to be proven. A checkmark \(\checkmark\) signals an available fact. A numeric prefix refers to a line number in the code: for the preceding code, 4.pre \(_3\) denotes the precondition clause pre \(_3\) of the feature (set_spouse) called at line 4. If there is no such prefix, then the fact is a contract element or an AS/BS component from the proof rule; for example, AS \(_1\) .o.inv \(_1\) states that inv \(_1\) holds for o, satisfying entry AS \(_1\) of the rule.

The full program text appears below. The body of make only consists of assignments and trivially establishes both its postcondition and the class invariant.

Verification of set_left and set_right is straightforward too—the assignments establish the postconditions, and the preconditions establish the invariants on exit. The generic parameter G represents the type of list elements.

Note that routine insert_between_two is “wrapped” by a public routine insert_right as the extra arguments of the first should be in internally called (secret) routine, so that the preconditions will be guaranteed.

The proofs of insert and remove appear below.

Class OBSERVER is a simple implementation of the Observer pattern.

The proof of OBSERVER.update is immediate: The postcondition follows from the assignment, and the AS \(_1\) .Current.inv \(_3\) obligation from assuming BS \(_1\) .Current.inv \(_3\) .

The code for the Subject in the Observer pattern is as follows:

Proving make and update_observer is trivial: All the proof goals imposed by the proof rule directly follow from these features’ preconditions and implementations, so we do not present them.