In this chapter we will study yet another kind of assertions called class invariants. The class invariant serves as a strengthening of both the preconditions and the postconditions of all operations in the class. As we will see in the first section of this chapter, a good class invariant makes it easier to formulate both preconditions and postconditions of the operations in the class.

52.1 General aspects of contracts 52.3 An example of a class invariant 52.2 Everyday invariants

 

52.1.  General aspects of contracts
Contents   Up Previous Next   Slide Annotated slide Aggregated slides    Subject index Program index Exercise index 

When we do computations in general, the values of the variables in the running programs are modified throughout the computation. In an object-oriented program the states of the involved objects will vary as the program execution progresses. This variation of the program state is not arbitrary, however. There is usually some rules that control and constrain the variations. Such rules can be formulated as invariants. An invariant describes some properties and relationships that remain constant (do not vary) during the execution of a program.

A class invariant is an assertion that captures the properties and relationships, which remain stable throughout the life-time of instances of the class.

The following characterizes a class invariant:

acts as a general strengthening of both the precondition and postcondition expresses a "health criterion" of the object must be fulfilled by the constructor must be maintained by the public operations must not necessarily be maintained by private and protected operations

The class invariant is an assertion, which should be true at every stable point in time during the life of an object. In this context, a stable point in time is just after the completion of the constructor and in between executions of public operations on the class. At a stable point in time, the object is in rest - the object is not in the middle of being updated. The unstable points in time are, for instance, in the middle of the execution of a constructor, or in the middle of the execution of a public operation. In addition, a non-public operation may leave the object in a state, which does not satisfy the class invariant. The reason is that a public operation may need to activate several non-public operations, and it may need to carry out additional state changes (assignments) in order to reach a stable state that satisfies the class invariant. A non-public operation may be responsible for only a fraction of the updating of an object.

You can think of the class invariant as a health criterion, which must be fulfilled by all objects in between operations. As a precondition of every public operation of the class, it can therefore be assumed that the class invariant holds. In addition, it can be assumed as a postcondition of every public operation that the class invariant holds. In this sense, the class invariant serves as a general strengthening of both the precondition and the postcondition of public operations in the class. The effective precondition is the formulated precondition in conjunction with the class invariant. Similarly, the effective postcondition is the formulated postcondition in conjunction with the class invariant.

Our primary interest in this chapter is class invariants. Invariants are, however, also useful and important in other contexts.

52.2.  Everyday invariants
Contents   Up Previous Next   Slide Annotated slide Aggregated slides    Subject index Program index Exercise index 

Before we proceed to a programming example, we will draw the attention to useful everyday invariants.

Coffee Machine In between operations there is always at least one cup of coffee available Toilet In between "transactions" there is always at least 0.75 meter of toilet paper on the roll Keys and wallet In between using keys and/or wallet During daytime: Keys and wallet are in the pocket During nighttime: Keys are wallet are located on the bedside table or underneath the pillow

The coffee machine invariant ensures that nobody will go for coffee in vain. If you happen to fill your jug with the last cup of coffee from the coffee pot, your operation on the coffee machine is not completed until you have brewed a new pot of coffee.

The toilet paper invariant should be broadly appreciated. As a consequence of the invariant, the operation of emptying the toilet paper reel is not completed before you have found and mounted an extra, full reel of paper.

The last everyday invariant is - in my experience - often broken by women and children, because they do not always wear practical cloth with pockets suitable for wallets and keys. As a consequence, these important items tend to be forgotten or misplaced, such that they are not available when needed. If the proposed key and wallet invariant is observed, you either use the key or wallet, or you will be confident where to find them.

52.3.  An example of a class invariant
Contents   Up Previous Next   Slide Annotated slide Aggregated slides    Subject index Program index Exercise index 

It is now time to study the invariant of the circular list. Recall that we introduced preconditions and postconditions of the circular list in Program 50.1 of Section 50.2.

The class invariant of a circular lists expresses that the list is circular whenever it is non-empty. In Program 52.1 the invariant is formulated at the bottom of the program, in line 43-45. In the same way as the preconditions and postconditions, the class invariant involves subexpressions that are realized by programmed operations (empty, isCircular, and size) of the class.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

class CircularList {

  // Construct an empty circular list 
  public CircularList()
    require true;   
    ensure empty();   

  // Return my number of elements 
  public int size()
    require true;   
    ensure (size = countElements) && noChange;   

  // Insert el as a new first element 
  public void insertFirst(Object el)
    require !full();   
    ensure !empty() && isFirst(el);   
     
  // Insert el as a new last element 
  public void insertLast(Object el)
    require !full();   
    ensure !empty() && isLast(el);     

  // Delete my first element 
  public void deleteFirst()
    require !empty();   
    ensure (empty() || isFirst(old retrieveSecond));   

  // Delete my last element 
  public void deleteLast()
    require !empty();   
    ensure (empty() || isLast(old retrieveButLast()));   

  // Return the first element in the list 
  Object retrieveFirst()
    require !empty();   
    ensure isFirst(result) && noChange;   

  // Return the last element in the list 
  Object retrieveLast()
    require !empty();   
    ensure isLast(result) && noChange;   

  invariant
    !empty() implies isCircular()  and
    empty() implies (size() = 0);   
}

If we compare Program 52.1 with Program 50.1 it is worth noticing that the preconditions and postconditions become simpler and shorter, because they implicitly assumes that the class invariant is true. Thus, relative to (a slightly idealised version of) Program 50.1, the invariant is factored out of all preconditions and postconditions.