[
https://issues.apache.org/jira/browse/GROOVY-11443?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Paul King closed GROOVY-11443.
------------------------------
> 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
> Fix For: 5.0.0-alpha-10
>
>
> Languages like Dafny support having multiple pre/post condition clauses. They
> are just and'd 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}
> The invariant for class C is "1 && 2 && 3 && 4 && 5 && 6" as is the
> postcondition.
> The precondition is "(1 && 2) || (3 && 4) || (5 && 6)". Preconditions are
> typically or'd like this to handle the weaker pre rule - no change in
> behavior was made, just and'ing together the terms in the one class/interface.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
