Groovy Stack Example With GContracts

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

@Invariant({ elements != null })
class Stack {
    
    private List elements
    
    @Ensures({ is_empty() })
    public Stack()  {
        elements = []
    }
    
    @Requires({ preElements?.size() > 0 })
    @Ensures({ !is_empty() })
    public Stack(List preElements)  {
        elements = preElements
    }
    
    def boolean is_empty()  {
        elements.isEmpty()
    }
    
    @Requires({ !is_empty() })
    def last_item()  {
        elements.last()
    }
    
    def count() {
        elements.size()
    }
    
    @Ensures({ result == true ? count() > 0 : count() >= 0  })
    def boolean has(def item)  {
        elements.contains(item)
    }
    
    @Ensures({ last_item() == item })
    def put(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()
    }
    
    def String toString() { elements.toString() }
}

def stack = new Stack([1,2,3,4,5])

post-condition for replace() should be:
@ensures({ last_item() == item })