[GROOVY-11238] Logical implication operator revisited - ASF JIRA

Attach files

Attach Screenshot

Voters

Watch issue

Watchers

Create sub-task

Link

Clone

Update Comment Author

Replace String in Comment

Update Comment Visibility

Delete Comments

XML

Word

Printable

JSON

Details

Type: New Feature
Status: Closed
Priority: Major
Resolution: Fixed
Affects Version/s: None
Fix Version/s: 5.0.0-alpha-4
Component/s: None
Labels:
None

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.