GContracts

@Grab('org.gcontracts:gcontracts-core:1.2.10') 
import org.gcontracts.annotations.*

@Contracted
@Invariant({ myspeed >= 0 })
class Rocket { 
    boolean moving = false
    int myspeed = 0
    
    @Requires({ !moving && myspeed == 0 })
    void start() { moving = true }
    
    @Requires({ moving && myspeed == 0 })
    void stop() { moving = false }
    
    @Requires({ moving })
    @Ensures({ old.myspeed < myspeed })
    void accelerate(Integer inc) {
        println ">>$inc"
        this.myspeed += inc ?: 1
    }
    
    @Requires({ isStarted() })
    @Ensures({ old.myspeed > myspeed })
    void deccelerate(Integer inc) {  
        println "<<$inc"
        this.myspeed -= inc ?: 1
    }

    
    private boolean isStarted() { return moving } 
    private int speed() { return myspeed }
}

def r = new Rocket()

//r.accelerate() //THIS WOULD FAIL
r.start()
r.accelerate()
println '==' + r.speed()
r.accelerate(2)
println '==' + r.speed()
//r.accelerate(-2) //THIS WOULD FAIL
r.deccelerate(2)
println '==' + r.speed()
//r.deccelerate(2) //THIS WOULD FAIL
//r.stop() //THIS WOULD FAIL
//r.start() //THIS WOULD FAIL
r.deccelerate(1)
r.stop()
r.start()
//r.deccelerate(1) //THIS WOULD FAIL
r.stop()

see: http://groovyconsole.appspot.com/script/449003