Hello!
I'm playing with the stack example and cofoja. I've got an ArrayList<T> implementation of the stacks and I'm trying to specify what it's not usually specified, ie, LIFO property. So I have:
private final ArrayList<T> elements;
@Ensures({
"elements.size() == old(elements.size()) + 1",
"isLifoPropertyFulfilled(old(elements))"
})
public void push(T elem) {
elements.add(elem);
}
My idea is to deep copy the actual structure (obtained from post execution of push method), then pop in it and finally to compare it with a deep copy of the initial structure (obtained from pre execution of push method). This initial structure should be 'old(elements)' but it doesn't work. I'm thinking that 'old' doesn't work in the same manner with value types than whith references types. Can you help me, please?
Thanks in advance. Best regards,
Jose Maria