How can class invariant strengthen pre and post-conditions?

Question

Link

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.

public class Server
{
     // other code ommited
    public Output Foo(Input cmdIn)
    {
        ...
        return cmdOut;
    }
}


public class Caller
{  
    // other code ommited

    /* calls Server.Foo */
    public void Call()
    {...}
}

public class Input
{
    // other code ommited

    public int Length
    {...}
}

public class Output
{
    // other code ommited

    public int Length
    {...}
}

1. If class invariant is defined on Server class:

a) Preconditions are typically formulated in terms of the formal parameters of the called operation, so how can class invariant strengthen method's ( Foo's ) preconditions?

b) Postcondition is formulated in terms of called method's return value, so how can class invariant strengthen method's ( Foo's ) postconditions?

2. Can class invariant defined on Caller class in any way strengthen Foo's preconditions or postconditions?

3. If class invariant is defined on Foo's cmdIn parameter:

a) If precondition on Foo states that cmdIn.Length is within range 1-20, but one of class invariants defined on Input states that Input.Length should be within range 2-19, then Foo's precondition was indeed strenghten?

b) Isn't the logic in a) a bit flawed, since if class invariant already states that Input.Length should be within range 2-19, isn't it then an error for Foo to define a precondition which isn't always be true ( cmdIn.Length can't hold values 1 or 20 )

c) But if class invariant defined on Input states that Input.Length should be within range 0-100, then Foo's precondition isn't strengthen?

d) Can class invariants defined on cmdIn also somehow strengthen Foo's postcondition?

4. If class invariant is defined on Foo's return value

a) If postcondition on Foo states that cmdOut.Length is within range 1-20, but one of class invariants defined on Output states that Output.Length should be within range 2-19, then Foo's postcondition was indeed strengthen?

b) But if invariant defined on Output states that Output.Length should be within range 0-100, then Foo's postcondition wasn't strengthen?

c) Can class invariants defined on Output also somehow strengthen Foo's precondition?

5. But I get the impression that quoted article meant to say that just by having a class invariant ( and even if this invariant doesn't in any way operate ( directly or indirectly ) on Foo's parameters and/or return value, it would still strengthen Foo's preconditions and postcondition? If that's what article is actually implying, how is that possible?

thanks

Answer 1

a) Preconditions are typically formulated in terms of the formal parameters of the called operation, so how can class invariant strengthen method's ( Foo's ) preconditions?

I suspect that's key to your misunderstanding. Pre-conditions may include formal parameters - but are not restricted to them. They can - and often do - also refer to class features (attributes/operations). In general, the combination of invariants and pre-condition defines a set of constraints that must be satisfied before an operation is obliged to meet its post-condition when called. Similarly, an operation must guarantee that both its post condition and any invariants will be satisfied when it completes. Take the example of a Bounded Buffer:

Class BoundedBuffer<T> {
   public int max    // max #items the buffer can hold
   public int count  // how many items currently in the buffer

   void push(T item) {...}
   T    pop() {...}
}

A pre-condition for push() would be that the buffer has not reached its maximum size:

 pre: count < max

So here the pre-condition doesn't even mention the operation's formal parameter. We can also state an invariant for the Buffer:

inv: count >=0  //can't have -ve number of elements in the buffer

It strengthens the pre-condition because it entends what must be true before the push() operation is obliged to meet its post condition. The two clauses are logically ANDed together. So the effective pre-condition is count >=0 AND count < max. That's a stronger (more restrictive) constraint than the pre-condition alone.

Note the concept isn't restricted to situations where the pre-condition refers to class features. Let's add the constraint that the size of any individual item being added to the buffer must be less than some upper limit:

pre: count < max AND item.size() <= MAX_ITEM_SIZE

Adding the invariant still strengthens the effective pre-condition to become:

pre: count < max AND item.size() <= MAX_ITEM_SIZE AND count >=0

So in summary: invariants must hold before an operation is invoked and after an operation completes. Hence they strengthen both.

1. Can class invariant defined on Caller class in any way strengthen Foo's preconditions or postconditions?

No. Invariants apply to the class they are defined on only.

Answers to your remaining questions flow logically from above.

hth.