[
https://issues.apache.org/jira/browse/GROOVY-11443?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Paul King updated GROOVY-11443:
-------------------------------
Description:
Languages like Dafny support having multiple pre/post condition clauses. They
are just and'ed together.
A contrived example (with boring constants as the conditions - but you'll get
the idea):
{code}
import groovy.contracts.*
@Invariant({ 1 })
@Invariant({ 2 })
interface F {
@Ensures({ 1 })
@Ensures({ 2 })
@Requires({ 1 })
@Requires({ 2 })
def foo()
}
@Invariant({ 3 })
@Invariant({ 4 })
abstract class P {
@Requires({ 3 })
@Requires({ 4 })
@Ensures({ 3 })
@Ensures({ 4 })
abstract def foo()
}
@Invariant({ 5 })
@Invariant({ 6 })
class C extends P implements F {
def d() { println new Date() }
@Requires({ 5 })
@Requires({ 6 })
@Ensures({ 5 })
@Ensures({ 6 })
def foo() { println true }
}
new C().d()
{code}
was:Languages like Dafny support having multiple pre/post condition clauses.
They are just and'ed together.
> Support multiple Requires/Ensures/Invariant annotations in groovy-contracts
> ---------------------------------------------------------------------------
>
> Key: GROOVY-11443
> URL: https://issues.apache.org/jira/browse/GROOVY-11443
> Project: Groovy
> Issue Type: Improvement
> Reporter: Paul King
> Assignee: Paul King
> Priority: Major
>
> Languages like Dafny support having multiple pre/post condition clauses. They
> are just and'ed together.
> A contrived example (with boring constants as the conditions - but you'll get
> the idea):
> {code}
> import groovy.contracts.*
> @Invariant({ 1 })
> @Invariant({ 2 })
> interface F {
> @Ensures({ 1 })
> @Ensures({ 2 })
> @Requires({ 1 })
> @Requires({ 2 })
> def foo()
> }
> @Invariant({ 3 })
> @Invariant({ 4 })
> abstract class P {
> @Requires({ 3 })
> @Requires({ 4 })
> @Ensures({ 3 })
> @Ensures({ 4 })
> abstract def foo()
> }
> @Invariant({ 5 })
> @Invariant({ 6 })
> class C extends P implements F {
> def d() { println new Date() }
> @Requires({ 5 })
> @Requires({ 6 })
> @Ensures({ 5 })
> @Ensures({ 6 })
> def foo() { println true }
> }
> new C().d()
> {code}
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
