Question about keyword 'old'

[José María]

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

[David "Morgan" Morgan]

Hi Jose,

As you've noticed, "old" only gives you surface level access to old data. Anything else would require a complete copy of the elements to be kept, which would be too expensive.

So you can't explicitly check the full stack behaviour; instead you'll need to guarantee the full stack behaviour as a combination of how the various operations behave.

Regards

David

--
You received this message because you are subscribed to the Google Groups "cofoja" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cofoja+un...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[José María]

Ok, I get it! Thank you very much, David!

Regards,

Jose