[GROOVY-11238] Logical implication operator revisited

• Type: New Feature
• Status: Closed
• Priority: Major
• Resolution: Fixed
• Fix Version/s: 5.0.0-alpha-4
• Assignee: Paul King
• Reporter: Paul King
• Created: 27/Nov/23 10:10
• Updated: 22/Dec/23 11:38
• Resolved: 28/Nov/23 22:16

Description

Some languages like Racket, Eiffel and Dafny have an implication operator. Others like Scala and Python rely on the "<=" operator for Booleans, though that is not short-circuiting. Groovy has an "implies" method (also short-circuiting) and we explored some time back about supporting an implication operator. At the time, we decided it wasn't needed, after all, "A implies B" is the same as "!A || B". In a lot of programming scenarios, the existing operators work well and are well known, but there are some cases like preconditions, postconditions, invariants and other logical expressions where the implication operator would read better. Since the groovy-contracts module supports such expressions and testing frameworks like jqwik also have logical expressions, this issue is to explore that possibility again.

Earlier, we had considered "=>" as the operator (like Racket) but that was considered too easy to confuse with "<=" and ">=". It also conflicted with the early lambda syntax (though that isn't relevant now). So, I suggest we use "==>" like Dafny (and what has been proposed for Scala).

Here is what some jqwik tests would look like:

@Property(tries=10)
boolean 'only zero is the same as the negative of itself'(@ForAll int i) {
    i == 0 ==> i == -i
}

@Property(tries=100)
boolean 'an odd number squared is still odd'(@ForAll int n) {
    n % 2 == 1 ==> (n ** 2) % 2 == 1
}

@Property(tries=100)
boolean 'abs of a positive integer is itself'(@ForAll int i) {
    i >= 0 ==> i.abs() == i
}

Here is an example with DBC:

@Requires({ result >= 0
  && (n >= 0 ==> result == n)
  && (n < 0 ==> result == -n)})
int myAbs(int n) {
    n.abs()
}

This is in a form that could be sent to a proof checking framework (though we have no such integration today).

So, to recap, the goal here is not to make wholesale changes to existing code which might use the existing operators, but to provide the "==>" operator for scenarios where the operator aids readability or otherwise makes sense.

Issue Links

• supercedes: GROOVY-2576 Add "implies" operator for boolean expressions
• links to: GitHub Pull Request #1999