[
https://issues.apache.org/jira/browse/GROOVY-11238?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Paul King updated GROOVY-11238:
-------------------------------
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:
{code:groovy}
@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
}
{code}
So, the goal here is not to make wholesale changes to existing code which might
use the existing operators, but to provide the "==>" operator for cases which
make sense.
> Logical implication operator revisited
> --------------------------------------
>
> Key: GROOVY-11238
> URL: https://issues.apache.org/jira/browse/GROOVY-11238
> Project: Groovy
> Issue Type: New Feature
> Reporter: Paul King
> Priority: Major
> Fix For: 5.x
>
>
> 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:
> {code:groovy}
> @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
> }
> {code}
> So, the goal here is not to make wholesale changes to existing code which
> might use the existing operators, but to provide the "==>" operator for cases
> which make sense.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
