GContracts: Inheritance of Pre- and Postconditions

GContracts 1.1.0 [0] introduced inheritance for pre- and postconditions and optimized class invariant inheritance. If you want to know more about GContracts take a look at the wiki [1] or at blog-posts tagged with "gcontracts".

What about postcondition inheritance?

Postconditions are used to specify what work is guaranteed by the supplier to be done in a specific method, under the condition that the precondition is satisfied. When inheritance comes into play, postconditions of a parent class are inherited by overridden methods of a descendant class. Imagine a class Stack which provides methods for modifying objects kept in LIFO order.

import org.gcontracts.annotations.*

@Invariant({ elements != null })
class Stack {

    private List elements

    @Ensures({ is_empty() })
    public Stack()  {
        elements = []
    }

    @Requires({ preElements?.size() > 0 })
    @Ensures({ !is_empty() })
    public Stack(List preElements)  {
        elements = preElements
    }

    def boolean is_empty()  {
        elements.isEmpty()
    }

    @Requires({ !is_empty() })
    def last_item()  {
        elements.last()
    }

    def count() {
        elements.size()
    }

    @Ensures({ result == true ? count() > 0 : count() >= 0  })
    def boolean has(def item)  {
        elements.contains(item)
    }

    @Ensures({ last_item() == item })
    def put(def item)  {
       elements.push(item)
    }

    @Requires({ !is_empty() })
    @Ensures({ last_item() == item })
    def replace(def item)  {
        remove()
        elements.push(item)
    }

    @Requires({ !is_empty() })
    @Ensures({ result != null })
    def remove()  {
        elements.pop()
    }

    def String toString() { elements.toString() }
}

As you can see in the code sample @Requires and @Ensures is used to specify pre- and postconditions in certain methods. Whenever an object of type Stack is used at runtime those assertions will be checked due to hidden code segments injected by GContracts at compile-time (under the assertion that Java's assert mechanism is activated via the command line argument -ea). Let's assume we need an extended Stack that provides us with changed method behavior. For example, we want to add a put method that adds inlining support for lists:

def stack = new Stack()
stack.push(['value1', 'value2', 'value3'])

In order to implement this feature we need to override the put method found in the parent class.

class GroovyStack extends Stack  {

    @Override
    def put(def item)  {
        if (item instanceof List) item.each { super.put(it) }
        else super.put(item)

        return item
    }
}

If we create an instance of GroovyStack and call put with a list as actual parameter, the following assertion violation appears:

[inherited postcondition] in method <put(item:java.lang.Object)> violated. Expression: (this.last_item() == item). Values: item = [1, 2, 3, 4]

A look at the original postcondition shows that this is in fact the case, since our new put method in the descendant flattens the given parameter and for each item in the given list executes the put method once. Maybe a new postcondition in the descendant will solve this issue:

class GroovyStack extends Stack  {

    @Override
    @Ensures({ item instanceof List ? item.last() == last_item() : item == last_item() })
    def put(def item)  {
        if (item instanceof List) item.each { super.put(it) }
        else super.put(item)

        return item
    }
}

Execution again shows the following assertion:

[inherited postcondition] in method <put(item:java.lang.Object)> violated. Expression: (this.last_item() == item). Values: item = [1, 2, 3, 4]

This leads us to the most important point with rewritten postconditions in descendant classes: you can't override them. A postcondition in a descendant class is always joined with the postcondition of the super class, the postcondition of the parent class is said to be strengthened. That means, an overridden method has to implement the postcondition of its parent classes AND its self-defined postcondition. This might seem awkward at first, but consider the following code:

Stack stack = StackFactory.getInstance()

stack.put([1,2,3,4])

The thing is, if we override the put method in the GroovyStack class the semantic of the code above would change with the type of Stack used at runtime: a Stack instance would push the complete list on the stack, a GroovyStack instance would push the single list items. Indeed, changing the behavior of an overridden method does not conform to the assertion that inheritance always resembles an is-a relationship. If a GroovyStack should be a Stack, than it has to implement all postconditions of its parent class in overridden methods to conform to the contracts that were specified in the parent and on which clients already might rely on. Due to inheritance of the parent postcondition we stumbled upon this circumstance and it made us think about how the Stack data-structure could already be used by its clients.

What about precondition inheritance?

Preconditions are used to specify certain conditions which must be fulfilled by a client so that a method call on an object succeeds. So far, GContracts did not support inheritance of preconditions, meaning that whenever a parent class defined a precondition on a method which has been overridden in a descendant, the precondition in the descendant had to be newly defined. In contrast with postconditions, preconditions weaken the parent's preconditions. Whenever a parent class defines a precondition on a method, an overridden method might define additional preconditions which might be fulfilled by a client, but don't have to be. If we would like to rewrite the replace method in GroovyClass we could specify an additional precondition:

   @Requires({ item != null })
    @Ensures({ item() == item })
    def replace(def item)  {
        super.replace(item)
    }

But that additional precondition weakens the original one, meaning that a call like remove(null) on GroovyStack would still suffice the precondition. In contrast, a put method call on an empty stack would still raise an AssertionError.

Conclusion

Inheritance of pre- and postconditions complements object-oriented mechanisms like polymorphism, dynamic binding and overriding methods and channels those concepts to correct uses. GContracts for Groovy finally supports precondition and postcondition with 1.1.0. Therefore it supports the main principles found in Design by Contract(tm) and allows to apply the full power of contracts to domain models in Groovy/Grails projects.