[
https://issues.apache.org/jira/browse/GROOVY-11238?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Paul King closed GROOVY-11238.
------------------------------
> 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.0.0-alpha-4
>
>
> 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)
