Groovy Goodness: Logical Implication Operator

Since Groovy 1.8.3 Groovy has an implies() method for Boolean types. Groovy 5 adds an operator ==> for this method so you have a shorter way to express a logical implication. A logical implication is a logical function that can be expressed as P ==> Q. You can read this as P implies Q or if P than Q. This expression is true in every case except when P is true, but Q is false. The following truth table shows the interpretaton of the logical implication operator:

P	Q	P ==> Q
false	true	true
false	false	true
true	true	true
true	false	false

In the following example you can see usage of the new operator:

// Logical implication operator
assert false ==> true
assert false ==> false
assert true ==> true
assert !(true ==> false)

// Method with the following logical implication:
// If x > 0 then y must be greater than x.
def positiveXimpliesYgreaterX(x, y){
  (x > 0) ==> y > x
}

assert positiveXimpliesYgreaterX(1, 2)
assert !positiveXimpliesYgreaterX(1, 1)
assert positiveXimpliesYgreaterX(0, 1)
assert positiveXimpliesYgreaterX(0, 0)

The new operator is very useful in combination with Groovy Contracts:

import groovy.contracts.Ensures
import org.apache.groovy.contracts.PostconditionViolation
import static groovy.test.GroovyAssert.shouldFail

// Ensures that method result is greater
// than argument x if x > 0 using the
// implies operator.
@Ensures({ x > 0 ==> result > x })
int incrementIfPositive(int x) {
  if (x > 0) {
    // Implementation is following the
    // the logical implication defined in
    // the @Ensures annotation.
    return x + 1
  } else {
    return x
  }
}

// Ensures that method result is greater
// than argument x if x > 0 using the
// implies operator.
@Ensures({ x > 0 ==> result > x })
int faultyIncrementIfPositive(int x) {
  if (x > 0) {
    // Implementation is not following the
    // the logical implication defined in
    // the @Ensures annotation.
    return x - 1
  } else {
    return x
  }
}

// main method to invoke methods annotated with @Ensures.
def main() {
  assert incrementIfPositive(1) == 2
  assert incrementIfPositive(0) == 0

  assert faultyIncrementIfPositive(0) == 0
  shouldFail(PostconditionViolation) {
    faultyIncrementIfPositive(1)
  }
}

Written with Groovy 5.0.0.