Contracts for Groovy

Tutorial - GContracts: A Design by Contract extension for Groovy - Part 2

 

Contract Element Part 1: Preconditions with @Requires

@Requires is supposed to be used for precondition specifications. It can only be applied on instance method, static method and interface method declarations. Listing 5 shows how our Rocket class looks like after manually transforming all assertion statements to preconditions.

 

import org.gcontracts.annotations.*

class Rocket  {

    int speed
    private boolean started
    
    @Requires()
    def start() { started = true }
    
    boolean isStarted() { started }
    
    @Requires({ started })
    def accelerate()  {
        speed = speed + 5
    }
    
    @Requires({ started })
    def brake() { 
        speed = speed - 5 
    }
}

 

As can be seen with respect to the refactored Rocket class, the introduction of @Requires for preconditions leads to much cleaner code, as all assertion code is moved to closure annotation parameters.

Code inside the closure annotation can access method parameters, publicly accessible instance variables and methods. If accelerate would come with a parameter dx indicating the speed delta, @Requires could be used to check for its validity, too.

Listing 6

 

@Requires({ started && dx > 0 })
def accelerate(int dx)  {
    speed = speed + dx
}

 

The contract author is free to use arbitrary Groovy language construct within the precondition, as long as the resulting code is a Boolean expression. Otherwise, GContracts will detect non-boolean expressions and will throw a compile-time error.

As already noted, another major benefit of using GContracts is its integration with inheritance and polymorphism. If we would enhance the AnotherRocket subclass by overwriting Rocket#accelerate() with a custom implementation, we wouldn't need to define the precondition again. It would simply be inherited as AnotherRocket is a Rocket descendant.

Listing 7

 

class AnotherRocket extends Rocket {
    def accelerate()  {  // @Requires will be inherited from Rocket
        speed = speed + 1
    }
}
    
def rocket = new AnotherRocket()
rocket.accelerate()

 

A call to AnotherRocket#accelerate() without a prior call to AnotherRocket#start() would fail with a slightly modified Groovy power assertion message:

 

org.gcontracts.PreconditionViolation: <org.gcontracts.annotations.Requires> Rocket.java.lang.Object accelerate()

 

started

|

false

 

 

The power assertion message shows the part of the contract that has been violated, shows the results of sub-expressions and points to the part of the Boolean expression being “false”. This works even better with complex Boolean expressions:

 

org.gcontracts.PreconditionViolation: <org.gcontracts.annotations.Requires> Rocket.java.lang.Object accelerate()

 

((1 + 1) * 3) == 7

    |    |    |

    2    6   false

 

 

 

In addition, GContracts supports redefining base class preconditions. A precondition redefinition can be achieved by providing an additional @Requires annotation to AnotherRocket#accelerate() (see Listing 8).

Listing 8

 

class AnotherRocket extends Rocket {

    @Requires({ !started })
    def accelerate()  { 
        speed = speed + 1
    }
}

 

During compilation, GContracts will join both preconditions to a single precondition. In order to still support inheritance and polymorphism, preconditions can only be weakened by subclasses, thus the precondition above would be equal to @Requires({ started || !started }) – an assertion always being “true”.

Contract Element Part 2: Postconditions with @Ensures

So far, we did not talk about the general concept of postconditions. As noted in the previous sections, preconditions are a way to set certain boundaries for clients using the class – postconditions invert that principle. A postcondition states what in turn is guaranteed by the class author as long as the precondition is satisfied.

GContracts provides @Ensures for defining postconditions. The annotation can be applied on instance method, static method and interface method declarations. Back to the Rocket class example. Postconditions could be added to Rocket#brake() and Rocket#accelerate(), to state that both methods change the rockets speed in either way.

Listing 9

 

import org.gcontracts.annotations.*

class Rocket  {
    int speed
    private boolean started
    
    @Requires()
    def start() { started = true }
    
    boolean isStarted() { started }
    
    @Requires({ started })
    @Ensures({ speed - old.speed == 5 })
    def accelerate()  {
        speed = speed + 5
    }
    
    @Requires({ started })
    @Ensures({ old.speed - speed == 5 })
    def brake() { 
        speed = speed - 5 
    }
}

 

 

The postcondition code in Listing 9 shows another DbC-specific feature available solely for postconditions: the old variable.

Inside @Ensures, a special variable named old is available. It holds the values of all typed instance variables of the current object. In our case, it holds the speed instance variable, which is used to exactly determine whether the speed has changed by 5.

There is a second variable available in closure annotation code being used to refer to the actual method's result – assuming the method's return type is not void – it is called result. If accelerate would return the current speed, we could refer the return value in @Ensures (see Listing 10).

Listing 10

 

@Requires({ started })
@Ensures({ result - old.speed == 5 })
def accelerate()  {
  speed = speed + 5
  return speed

 

As it is the case with @Requires, all postconditions are populated down the inheritance hierarchy and multiple postconditions on a single method will automatically be merged during the compilation process. In contrast to preconditions, the merging rule for postconditions is such that postconditions down the class hierarchy can only strengthen the base class postcondition, never weaken it.

Contract Element Part 3: Class Invariants with @Invariant

So far for our Rocket class ... but wait. What happens if we call Rocket#brake() multiple times without ever calling Rocket#accelerate()? Right, the speed would turn smaller than zero. But as it turns out, speed must never be smaller than zero, being a formative property of Rocket objects.

A property that has to be fulfilled throughout the entire object life-time is called the class invariant. Class invariants can be specified with @Invariant. Again, the annotation uses a single closure annotation parameter and again the contract element is inherited to all direct and indirect subclasses.

Listing 11

 

@Invariant({ speed >= 0 && speed <= Integer.MAX_VALUE - 5 })
class Rocket  { ... } 

def rocket = new Rocket()
rocket.start()
rocket.accelerate()
rocket.brake()
rocket.brake() // fails with ClassInvariantViolation messsage

 

As you might have noticed, the speed instance variable isn't a real instance variable, it is a plain-old Groovy object property. GContracts automatically adds class invariant checks for all property accessor methods, so calling rocket.speed = -1 would again result in a class invariant violation.

Contracts, contracts, everywhere ...

GContracts becomes truly powerful when using its annotations in library or framework base classes. As it supports contract annotations on Groovy interfaces and abstract classes, this is can be done straight-forward.

Let us introduce a RocketAPI embedding the general contract directly in the interface definition.

Listing 12

 

import org.gcontracts.annotations.*

interface RocketAPI {
  def start()
  boolean isStarted()
  int getSpeed()
    
  @Requires({ started })
  @Ensures({ result - old.speed == 5 })
  def accelerate()
    
  @Requires({ started })
  @Ensures({ old.speed - speed == 5 })
  def brake()  
}

@Invariant({ speed >= 0 && speed <= Integer.MAX_VALUE - 5 })
class Rocket implements RocketAPI  {

    int speed
    private boolean started
    
    def start() { started = true }
    boolean isStarted() { started }
    
    def accelerate()  {
        speed = speed + 5
        return speed
    }
    
    def brake() { 
        speed = speed - 5 
    }
}

def rocket = new Rocket()
rocket.accelerate()

 

As a result, all classes implementing the RocketAPI interface must adhere to the specified contract. As said earlier, preconditions can only be weakened, postconditions can only be strengthened by implementation classes.

A call to Rocket#accelerate() without a preceding call to Rocket#start() would now fail with the following violation message:

 

org.gcontracts.PreconditionViolation: <org.gcontracts.annotations.Requires> RocketAPI.java.lang.Object accelerate() 

started
|
false

 

Notice that the error message’s originator has changed to RocketAPI#accelerate(). As the contract elements will be embedded in the resulting bytecode, we could put the RocketAPI into a jar and every project including the jar and GContracts would automatically be forced to comply with the specified contract.

Conclusion

This article only showed a selection of the most important core features of GContracts, with focus on the core contract annotations: @Requires, @Ensures and @Invariant.

More information on advanced features like the custom Groovydoc Ant task for embedding contracts into GroovyDoc generated class documentation, custom micro contract annotations for reusing small but reoccurring contract elements and disabling contracts on package- and class-level can be found at GContracts project wiki.

To start playing with contracts, download the most recent version (as of March 2012, 1.2.5) available on the project homepage or Maven central repository, add it to the applications classpath, import org.gcontracts.annotations – and your favourite programming language will magically support Design by Contract.

Design by Contract™ is a registered trademark of Interactive Software Engineering Inc.

 

Author Bio: 

Andre Steingress works as Groovy & Grails developer in Linz, Austria. He regularly blogs at http://blog.andresteingress.com, holds workshops and trainings focusing on Groovy, Grails and Spring, enjoys contributing to the Groovy programming language and is the creator of GContracts, a Design by Contract library for Groovy.

This article originally appeared in Java Tech Journal - The Groovy Universe. Check out the rest of that issue here

 

Pages

Andre Steingress

What do you think?

JAX Magazine - 2014 - 06 Exclucively for iPad users JAX Magazine on Android

Comments

Latest opinions