[
https://issues.apache.org/jira/browse/GROOVY-11238?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17790249#comment-17790249
]
Paul King commented on GROOVY-11238:
------------------------------------
The implies method, while useful in these scenarios, doesn't offer
short-circuiting. If the _consequent_ is expensive to calculate, that is wasted
cycles if the _precedent_ is false.
The forward arrow is the mathematical symbol. Of the other options, both "-->"
and "=>" have possibly worse problems. When I go look at the Dafny or Eiffel
books, implication is used often but they typically don't have too much
asciiart in play. I just picked the "i == 0 ==> i == -1" example because of its
simplicity.
If I take a more typical example from the Dafny book, and combine the syntax
from jqwik and groovy-contracts (since we don't have the exact equivalent of
Dafny as of today at least):
{code:java}
@Ensures(@ForAll int i, @ForAll int j, { i, j ->
i <= j ==> result[i] <= result[j]
})
List<String> sort(List<String> items) {
// sort method here
}
{code}
I looked at how Dafny gave precedence and how its expressions look when picking
precedence. Implication (in the current PR) has slightly higher precedence than
ternary/elvis. So for your examples, the following are the same (ternary is
right associative):
{code}
println a?b:c ==> d?e:f
println a?b: ((c ==> d) ?e:f)
{code}
{code}
println a ? b==>c : d==>e
println a ? (b==>c) : (d==>e)
{code}
Hmmm. The implication operator is right associative in Dafny but antlr's
default is left associative. I should probably change that. Dafny also has a
reverse implication operator "<==" (which is left associative) but I wasn't
proposing to support that.
Having said all that, I think combining multiple levels of complex operators
can lead to very asciiart looking code and probably warrants refactoring into
simpler expressions.
As for the precedence being the same for the Types#getPrecedence method, I
don't think we use that but have left it there for outside tools. I guess I
could make it slightly higher than ternary, but perhaps we deprecate that
method altogether?
> 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
> Assignee: 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}
> Here is an example with DBC:
> {code:groovy}
> @Requires({ result >= 0
> && (n >= 0 ==> result == n)
> && (n < 0 ==> result == -n)})
> int myAbs(int n) {
> n.abs()
> }
> {code}
> 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.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
