An old topic (pun intended)

[Timon Gehr]

On 10/17/2011 08:04 AM, Jonathan M Davis wrote:
> On Monday, October 17, 2011 00:29:30 Timon Gehr wrote:
>> On 10/16/2011 07:31 PM, Jonathan M Davis wrote:
>>> On Sunday, October 16, 2011 19:13:09 Timon Gehr wrote:
>>>> I don't agree that 'old' is very difficult to implement. Just evaluate
>>>> what is inside the 'old' before you enter the in contract, store
>>>> somewhere, maybe in hidden local variables, and make the data
>>>> available
>>>> in the out contract. Eiffel's 'old' does not do more than that.
>>>>
>>>> (but perhaps there are implementation details in DMD that make this
>>>> more
>>>> difficult than necessary. I don't know.)
>>>
>>> What if you're dealing with a class? You'd need to deep copy the entire
>>> object for it to work. There's no way built into the language to do
>>> that (not to mention that it would be horrifically inefficient).
>>>
>>> - Jonathan M Davis
>>
>> Eiffel does not do that either.
>> (even though it _does_ have a built in deep copy feature)
>>
>> We don't have to over-engineer the feature, if somebody needs to
>> deep-copy an object they can implement it themselves and use
>> old(obj.deepCopy()).
>
> I don't see how you could really expect to test the current state against the
> initial state when you don't actually save the initial state.

There are practical examples where this would be required but most of 
the time the tests are simple enough that the old expression can carry 
all the state you need. Remember that all implementations of DbC that 
have prestate (and I am aware of) don't perform a deep copy automatically.

Eg:

abstract class Set{
     @property int size();
     bool contains(int x);
     void insert(int x)
       out{ assert( old(contains(x)) && size == old(size) ||
                   !old(contains(x)) && size == old(size)+1);
            assert(contains(old(x)));
            // possibly also require that everything that was
            // in the set before is still there
            [...]
       }
}



> And as far as
> implementing it yourself goes, you could go and do that that right now. You
> don't need compiler support to save the initial state somewhere and then test
> against it afterwards. It's just nicer if the compiler gives you support for
> it.
>
> - Jonathan M Davis

As far as implementing it myself goes I could even do contract 
programming in the brainF programming language. =)

The feature adds a lot of value to contract programming. I use contract 
programming occasionally and almost every contract I add eventually 
detects small bugs during the testing of new code parts.

BTW: "Somewhere" would have to be on the execution stack because the 
function could be recursive. There is no way to refer to variables 
defined in the in contract from the out contract and doing the saving at 
any other place than in a contract is not acceptable for obvious reasons.