#31 ✓hold
me (at andresteingress)

cyclic class in preconditions

Reported by me (at andresteingress) | June 13th, 2011 @ 11:15 AM | in 1.2.5 (closed)

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

Comments and changes to this ticket

Please Sign in or create a free account to add a new ticket.

With your very own profile, you can contribute to projects, track your activity, watch tickets, receive and update tickets through your email and much more.

New-ticket Create new ticket

Create your profile

Help contribute to this project by taking a few moments to create your personal profile. Create your profile »

core module

Shared Ticket Bins

People watching this ticket

Pages