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.
