[GROOVY-11443] Support multiple Requires/Ensures/Invariant annotations in groovy-contracts

• Type: Improvement
• Status: Closed
• Priority: Major
• Resolution: Fixed
• Fix Version/s: 5.0.0-alpha-10
• Assignee: Paul King
• Reporter: Paul King
• Created: 17/Jul/24 09:49
• Updated: 12/Nov/24 11:40
• Resolved: 23/Jul/24 04:57

Description

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):

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()

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.

Issue Links

• links to: GitHub Pull Request #2100