org.jmlspecs.samples.stacks
Interface BoundedThing

All Known Subinterfaces:

BoundedStackInterface

All Known Implementing Classes:

BoundedStack

@ModelDefinitions(value={@Model(value="public instance int MAX_SIZE;"),@Model(value="public instance int size;")})
@InvariantDefinitions(value={@Invariant(header="public instance",value="MAX_SIZE > 0;"),@Invariant(header="public instance",value="0 <= size && size <= MAX_SIZE;")})
@Constraint(header="public instance",
            value="MAX_SIZE == #old(MAX_SIZE);")
public interface BoundedThing

Method Summary

java.lang.Object	clone()
int	getSizeLimit()
boolean	isEmpty()
boolean	isFull()

Method Detail

getSizeLimit

@SpecCase(header="public normal_behavior",
          ensures="#result == MAX_SIZE;")
@Pure
int getSizeLimit()

isEmpty

@SpecCase(header="public normal_behavior",
          ensures="#result <==> size == 0;")
@Pure
boolean isEmpty()

isFull

@SpecCase(header="public normal_behavior",
          ensures="#result <==> size == MAX_SIZE;")
@Pure
boolean isFull()

clone

@Also(value=@SpecCase(header="public behavior",assignable="#nothing;",ensures="#result instanceof BoundedThing&& size == ((BoundedThing)#result).size;",signalsOnly="CloneNotSupportedException;"))
java.lang.Object clone()
                       throws java.lang.CloneNotSupportedException

Throws:

java.lang.CloneNotSupportedException