Gcontracts gcontracts-core → 1.2.5

is_empty and is_full have cyclic calls in their preconditions. the precondition of the other method must not be checked in order to get fulfilled:

@Grab(group='org.gcontracts', module='gcontracts-core', version='[1.2.4,)')
import org.gcontracts.annotations.*

@Invariant({ elements != null })
class Stack {

    def elements

    @Ensures({ is_empty() })
    def Stack()  {
        elements = []
    }

    @Requires({ preElements?.size() > 0 })
    @Ensures({ !is_empty() })
    def Stack(List preElements)  {
        elements = preElements
    }

    @Requires({ !is_full() })
    boolean is_empty()  {
        elements.isEmpty()
    }
    
    @Requires({ !is_empty() })
    boolean is_full()  {
        false
    }

    @Requires({ !is_empty() })
    def last_item()  {
        elements.last()
    }

    def count() {
        elements.size()
    }

    @Ensures({ result == true ? count() > 0 : count() >= 0  })
    boolean has(def item)  {
        elements.contains(item)
    }

    @Ensures({ last_item() == item })
    def push(def item)  {
       elements.push(item)
    }

    @Requires({ !is_empty() })
    @Ensures({ last_item() == item })
    def replace(def item)  {
        remove()
        elements.push(item)
    }

    @Requires({ !is_empty() })
    @Ensures({ result != null })
    def remove()  {
        elements.pop()
    }

    String toString() { elements.toString() }
}

def stack = new Stack()
stack.is_empty()