www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Communicating between in and out contracts

reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Consider a Stack interface:

interface Stack(T) {
    bool empty();
    ref T top();
    void push(T value);
    void pop();
    size_t length();
}

Let's attach contracts to the interface:

interface Stack(T) {
    bool empty();
    ref T top()
    in {
       assert(!empty());
    }
    void push(T value);
    out {
       assert(value == top());
    }
    void pop()
    in {
       assert(!empty());
    }
    size_t length()
    out(result) {
       assert((result == 0) == empty());
    }
}

So far so good. The problem is now that it's impossible to express the
contract "the length after push() is the length before plus 1."

Eiffel offers the "old" keyword that refers to the old object in a
postcondition. But it seems quite wasteful to clone the object just to
have a contract look at a little portion of the old object.

I was thinking of having the two contracts share the same scope. In that
case we can write:

    void push(T value);
    in {
       auto oldLength = length();
    }
    out {
       assert(value == top());
       assert(length == oldLength + 1);
    }

Walter tried to implement that but it turned out to be very difficult
implementation-wise. We tossed around a couple of other ideas, without
making much progress. In particular inlining the contract bodies looks
more attractive than it really is. If you have any suggestion, please share.


Thanks,

Andrei
Oct 14 2009
next sibling parent reply Lutger <lutger.blijdestijn gmail.com> writes:
Between sharing the whole object and sharing scope lies specifying exactly 
what to share, I'd think.

Here is one possible syntax, like regular function calls. Parameter types 
can possibly be inferred and omitted:

void push(T value);
in {
   out(length());
}
out(size_t oldLength) {
   assert(value == top());
   assert(length == oldLength + 1);
}
Oct 14 2009
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Lutger wrote:
 Between sharing the whole object and sharing scope lies specifying exactly 
 what to share, I'd think.
 
 Here is one possible syntax, like regular function calls. Parameter types 
 can possibly be inferred and omitted:
 
 void push(T value);
 in {
    out(length());
 }
 out(size_t oldLength) {
    assert(value == top());
    assert(length == oldLength + 1);
 }

I think this could work. One of Walter's ideas was to pass the entire old object as an argument to out. Passing handpicked data is more work for the user but faster. Perhaps this would simplify things a bit: void push(T value); in { auto oldLength = length; } out(oldLength) { assert(value == top()); assert(length == oldLength + 1); } Whatever parameters you pass to out they'd be matched by name with stuff defined in the "in" contract. That poses a problem because until now out(whatever) automatically passed the result to the out contract under the name "whatever". Andrei
Oct 14 2009
parent Lutger <lutger.blijdestijn gmail.com> writes:
Andrei Alexandrescu wrote:

 Lutger wrote:
 Between sharing the whole object and sharing scope lies specifying
 exactly what to share, I'd think.
 
 Here is one possible syntax, like regular function calls. Parameter types
 can possibly be inferred and omitted:
 
 void push(T value);
 in {
    out(length());
 }
 out(size_t oldLength) {
    assert(value == top());
    assert(length == oldLength + 1);
 }

I think this could work. One of Walter's ideas was to pass the entire old object as an argument to out. Passing handpicked data is more work for the user but faster. Perhaps this would simplify things a bit: void push(T value); in { auto oldLength = length; } out(oldLength) { assert(value == top()); assert(length == oldLength + 1); } Whatever parameters you pass to out they'd be matched by name with stuff defined in the "in" contract. That poses a problem because until now out(whatever) automatically passed the result to the out contract under the name "whatever". Andrei

Right, I forgot about that, you do need that return variable or have to invent a magic name. Jeremie's proposal doesn't have that problem, taking the reverse route of letting in{} define which variabeles are to be passed to the out function. So either would work: in{ auto oldLength = length; out(oldLength); } or: in{ out auto oldLength = length; } Whatever syntax is chosen, it doesn't strike me as cumbersome to handpick variables considering what you get from it. Also, some conditions may depend on calculated values, in those cases it may even be more straightforward than checking an old copy of the object.
Oct 14 2009
prev sibling parent Jeremie Pelletier <jeremiep gmail.com> writes:
Lutger wrote:
 Between sharing the whole object and sharing scope lies specifying exactly 
 what to share, I'd think.
 
 Here is one possible syntax, like regular function calls. Parameter types 
 can possibly be inferred and omitted:
 
 void push(T value);
 in {
    out(length());
 }
 out(size_t oldLength) {
    assert(value == top());
    assert(length == oldLength + 1);
 }
 

I like this, but I wouldnt make a regular function call: void push(T value) in { out auto oldLength = length(); } out { assert(value == top()); assert(length() == oldLength + 1); } body { ... } If you declare variables as 'out' in a precondition, they are hidden from the body and visible in the post condition. The implementation of this is as easy as pushing oldLength on the stack in the precondition and poping it in the postcondition. Jeremie
Oct 14 2009
prev sibling next sibling parent Chris Nicholson-Sauls <ibisbasenji gmail.com> writes:
Andrei Alexandrescu wrote:
 Consider a Stack interface:
 
 interface Stack(T) {
    bool empty();
    ref T top();
    void push(T value);
    void pop();
    size_t length();
 }
 
 Let's attach contracts to the interface:
 
 interface Stack(T) {
    bool empty();
    ref T top()
    in {
       assert(!empty());
    }
    void push(T value);
    out {
       assert(value == top());
    }
    void pop()
    in {
       assert(!empty());
    }
    size_t length()
    out(result) {
       assert((result == 0) == empty());
    }
 }
 
 So far so good. The problem is now that it's impossible to express the
 contract "the length after push() is the length before plus 1."
 
 Eiffel offers the "old" keyword that refers to the old object in a
 postcondition. But it seems quite wasteful to clone the object just to
 have a contract look at a little portion of the old object.
 
 I was thinking of having the two contracts share the same scope. In that
 case we can write:
 
    void push(T value);
    in {
       auto oldLength = length();
    }
    out {
       assert(value == top());
       assert(length == oldLength + 1);
    }
 
 Walter tried to implement that but it turned out to be very difficult
 implementation-wise. We tossed around a couple of other ideas, without
 making much progress. In particular inlining the contract bodies looks
 more attractive than it really is. If you have any suggestion, please 
 share.
 
 
 Thanks,
 
 Andrei

How hard would it be to do something like this: collect any local variables declared in the precondition into a structure, and make that structure transparently available to the postcondition. So your push case above gets rewritten to something like this: __magic_tmp = { typeof( length() ) oldLength; } in { __magic_tmp.oldLength = length(); } out { assert(value == top()); assert(length == __magic_tmp.oldLength + 1); } Honestly Lutger's idea of passing the data like parameters might be better, I'm just somehow uneasy about the look of "out(foo,bar)". -- Chris Nicholson-Sauls
Oct 14 2009
prev sibling next sibling parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 Eiffel offers the "old" keyword that refers to the old object in a
 postcondition. But it seems quite wasteful to clone the object just to
 have a contract look at a little portion of the old object.

You don't need to clone the whole object. You just need to cache the properties that are used with 'old'. In other words, this functionality:
    void push(T value);
    in {
       auto oldLength = length();
    }
    out {
       assert(value == top());
       assert(length == oldLength + 1);
    }

...can be expressed with this syntax: void push(T value); out { assert(value == top()); assert(length == old length + 1); } The syntax with 'old' is more concise, easier to read, and does the same thing. What's wrong with it (other than adding yet another keyword to the language)? -- Rainer Deyke - rainerd eldwood.com
Oct 14 2009
next sibling parent reply Walter Bright <newshound1 digitalmars.com> writes:
Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 Eiffel offers the "old" keyword that refers to the old object in a
 postcondition. But it seems quite wasteful to clone the object just to
 have a contract look at a little portion of the old object.

You don't need to clone the whole object. You just need to cache the properties that are used with 'old'.

That's a good idea.
Oct 16 2009
next sibling parent bearophile <bearophileHUGS lycos.com> writes:
Walter Bright:

 Rainer Deyke:
 You don't need to clone the whole object.  You just need to cache the
 properties that are used with 'old'.

That's a good idea.

Once in a time I want to improve Walter's mood. This is a list of the top 25 requests for improvements to the Java language (some of them are about 10 years old, so people like me that complain that Walter isn't implementing their ideas have to compare the situation with the Sun engineers that sometimes look like molass): http://bugs.sun.com/bugdatabase/top25_rfes.do The top request, with 592 votes, submitted originally 23-APR-2001, asks for "Support For 'Design by Contract', beyond "a simple assertion facility"". I don't know if D programmers like to use such contracts often, but it seems several Java programmers wants them (even if in Java there are already ways to write unit tests that are far better&more flexible than D ones!). Bye, bearophile
Oct 16 2009
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Walter Bright wrote:
 Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 Eiffel offers the "old" keyword that refers to the old object in a
 postcondition. But it seems quite wasteful to clone the object just to
 have a contract look at a little portion of the old object.

You don't need to clone the whole object. You just need to cache the properties that are used with 'old'.

That's a good idea.

Should work, but it has more than a few subtleties. Consider: class A { int fun() { ... } int gun(int) { ... } int foo() in { } out(result) { if (old.fun()) assert(old.gun(5)); else assert(old.fun() + old.gun(6)); foreach (i; 1 .. old.fun()) assert(gun(i * i)); } ... } Now please tell what's cached and in what order. Andrei
Oct 16 2009
next sibling parent reply Jason House <jason.james.house gmail.com> writes:
Andrei Alexandrescu Wrote:

 Walter Bright wrote:
 Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 Eiffel offers the "old" keyword that refers to the old object in a
 postcondition. But it seems quite wasteful to clone the object just to
 have a contract look at a little portion of the old object.

You don't need to clone the whole object. You just need to cache the properties that are used with 'old'.

That's a good idea.

Should work, but it has more than a few subtleties. Consider: class A { int fun() { ... } int gun(int) { ... } int foo() in { } out(result) { if (old.fun()) assert(old.gun(5)); else assert(old.fun() + old.gun(6)); foreach (i; 1 .. old.fun()) assert(gun(i * i)); } ... } Now please tell what's cached and in what order. Andrei

if fun or gun is impure, then they should not be callable by the contracts. Because of that, order is irrelevant.
Oct 16 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Jason House wrote:
 if fun or gun is impure, then they should not be callable by the
 contracts. Because of that, order is irrelevant.

1. Restricting calls to pure functions is sensible, but was deemed too restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei
Oct 16 2009
next sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Denis Koroskin wrote:
 On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2korden gmail.com> 
 wrote:
 
 On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2korden gmail.com> 
 wrote:

 On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu 
 <SeeWebsiteForEmail erdani.org> wrote:

 Jason House wrote:
 if fun or gun is impure, then they should not be callable by the
 contracts. Because of that, order is irrelevant.

1. Restricting calls to pure functions is sensible, but was deemed too restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei

When not just let users one variable of type Variant per contract to store whatever they want?

I mean, not a Variant, but a Dynamic* object so that the following would be possible: void push(T)(T val) in(storage) { storage.oldSize = this.size; // store //storage.anyDynamicProperty = anyDynamicValue; in general case } out(storage) { assert(storage.oldSize + 1 == this.size); // access } body { // impl } *do you recall the Dynamic class discussion (a class that allows any arbitrary methods and properties access, similar to JavaScript objects or dynamic objects in C#)

On second thought Dynamic objects need run-time reflection that D currently lacks. Alternatively users may be given a Variant[string] assoc.array as a poor-man's replacement for a full-fledged Dynamic object: void push(T)(T val) in(storage) { storage["oldSize"] = this.size(); } out(storage) { assert(*storage["oldSize"].peek!(int) == this.size - 1); } body { // impl } The contracts userdata would be stored in a stack alongside with monitor, classinfo etc for classes, and past the data fields for structs.

I like this solution. Andrei
Oct 16 2009
prev sibling next sibling parent Jason House <jason.james.house gmail.com> writes:
Andrei Alexandrescu Wrote:

 Jason House wrote:
 if fun or gun is impure, then they should not be callable by the
 contracts. Because of that, order is irrelevant.

1. Restricting calls to pure functions is sensible, but was deemed too restrictive.

I don't know about others, but my use of contracts have always been pure. If my contracts violate that, then they're serving some other purpose and probably should not be a contract in the first place.
 2. Even so, there's difficulty on what to cache. The amount cached may 
 depend on both the old and new object (in my example it only depends on 
 the old object).
 
 3. There's too much hidden work and too much smarts involved. I just 
 don't think that's a feasible solution with what we know and have right now.

You never asked if it was too much work for Walter ;) Honestly, I think it may be simple enough to allow static (immutable) variable declarations within the in contract to be seen in the out contract. Maybe it isn't done with the static keyword. in{ keep oldLength = length; ... } out{ assert(oldLength == length + 1; }
Oct 16 2009
prev sibling parent reply Lutger <lutger.blijdestijn gmail.com> writes:
Denis Koroskin wrote:

 On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2korden gmail.com>
 wrote:
 
 On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2korden gmail.com>
 wrote:

 On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu
 <SeeWebsiteForEmail erdani.org> wrote:

 Jason House wrote:
 if fun or gun is impure, then they should not be callable by the
 contracts. Because of that, order is irrelevant.

1. Restricting calls to pure functions is sensible, but was deemed too restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei

When not just let users one variable of type Variant per contract to store whatever they want?

I mean, not a Variant, but a Dynamic* object so that the following would be possible: void push(T)(T val) in(storage) { storage.oldSize = this.size; // store //storage.anyDynamicProperty = anyDynamicValue; in general case } out(storage) { assert(storage.oldSize + 1 == this.size); // access } body { // impl } *do you recall the Dynamic class discussion (a class that allows any arbitrary methods and properties access, similar to JavaScript objects or dynamic objects in C#)

On second thought Dynamic objects need run-time reflection that D currently lacks. Alternatively users may be given a Variant[string] assoc.array as a poor-man's replacement for a full-fledged Dynamic object: void push(T)(T val) in(storage) { storage["oldSize"] = this.size(); } out(storage) { assert(*storage["oldSize"].peek!(int) == this.size - 1); } body { // impl } The contracts userdata would be stored in a stack alongside with monitor, classinfo etc for classes, and past the data fields for structs.

What is the benefit of variants here? Maybe I'm missing something, it just seems a little verbose and lose out on the type system (IDE support and such). Wouldn't it also tie the variant type to the language or is that not a problem?
Oct 16 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Lutger wrote:
 Denis Koroskin wrote:
 
 On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2korden gmail.com>
 wrote:

 On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2korden gmail.com>
 wrote:

 On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu
 <SeeWebsiteForEmail erdani.org> wrote:

 Jason House wrote:
 if fun or gun is impure, then they should not be callable by the
 contracts. Because of that, order is irrelevant.

restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei

store whatever they want?

be possible: void push(T)(T val) in(storage) { storage.oldSize = this.size; // store //storage.anyDynamicProperty = anyDynamicValue; in general case } out(storage) { assert(storage.oldSize + 1 == this.size); // access } body { // impl } *do you recall the Dynamic class discussion (a class that allows any arbitrary methods and properties access, similar to JavaScript objects or dynamic objects in C#)

currently lacks. Alternatively users may be given a Variant[string] assoc.array as a poor-man's replacement for a full-fledged Dynamic object: void push(T)(T val) in(storage) { storage["oldSize"] = this.size(); } out(storage) { assert(*storage["oldSize"].peek!(int) == this.size - 1); } body { // impl } The contracts userdata would be stored in a stack alongside with monitor, classinfo etc for classes, and past the data fields for structs.

What is the benefit of variants here? Maybe I'm missing something, it just seems a little verbose and lose out on the type system (IDE support and such). Wouldn't it also tie the variant type to the language or is that not a problem?

The nice thing there is that you have a single type to be a generic bag for any types. Andrei
Oct 16 2009
parent Lutger <lutger.blijdestijn gmail.com> writes:
Andrei Alexandrescu wrote:

 Lutger wrote:

 
 What is the benefit of variants here? Maybe I'm missing something, it
 just seems a little verbose and lose out on the type system (IDE support
 and such). Wouldn't it also tie the variant type to the language or is
 that not a problem?

The nice thing there is that you have a single type to be a generic bag for any types. Andrei

How? I mean that is a property of variants in general. Pre- and postconditions are written next to each other. I don't see anything generic about them, what am I missing? Let me rephrase that: if I have to write '*storage["oldSize"].peek!(int) == ...' in the out contract as opposed to just 'oldSize == ...', how would that be a win?
Oct 17 2009
prev sibling next sibling parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 class A {
     int fun() { ... }
     int gun(int) { ... }
 
     int foo()
     in {
     }
     out(result) {
         if (old.fun())
            assert(old.gun(5));
         else
            assert(old.fun() + old.gun(6));
         foreach (i; 1 .. old.fun())
            assert(gun(i * i));
     }
     ...
 }
 
 Now please tell what's cached and in what order.

The following are cached, in this order: fun() gun(5) gun(6) Old values are calculated in the order in which they appear in the function, but only once each. However, I strongly prefer the following syntax: class A { int fun() { ... } int gun(int) { ... } int foo() in { } out(result) { if (old(fun())) assert(old(gun(5))); else assert(old(fun()) + old(gun(6))); foreach (i; 1 .. old(fun())) assert(gun(i * i)); } ... } This lets you distinguish between the following cases: old(f().g()) old(f()).g() It also lets you cache non-members: old(arg); old(global_var); For example: void increment_global_counter() out { global_counter = old(global_counter) + 1; } -- Rainer Deyke - rainerd eldwood.com
Oct 16 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 class A {
     int fun() { ... }
     int gun(int) { ... }

     int foo()
     in {
     }
     out(result) {
         if (old.fun())
            assert(old.gun(5));
         else
            assert(old.fun() + old.gun(6));
         foreach (i; 1 .. old.fun())
            assert(gun(i * i));
     }
     ...
 }

 Now please tell what's cached and in what order.

The following are cached, in this order: fun() gun(5) gun(6) Old values are calculated in the order in which they appear in the function, but only once each.

Rats, I meant assert(old.gun(i * i)). That's what compounds the difficulty of the example.
 However, I strongly prefer the following syntax:
 
   class A {
       int fun() { ... }
       int gun(int) { ... }
 
       int foo()
       in {
       }
       out(result) {
           if (old(fun()))
              assert(old(gun(5)));
           else
              assert(old(fun()) + old(gun(6)));
           foreach (i; 1 .. old(fun()))
              assert(gun(i * i));
       }
       ...
   }
 
 This lets you distinguish between the following cases:
   old(f().g())
   old(f()).g()
 
 It also lets you cache non-members:
   old(arg);
   old(global_var);
 
 For example:
 
   void increment_global_counter() out {
     global_counter = old(global_counter) + 1;
   }

I honestly believe the whole "old" thing can't be made to work. Shall we move on to other possibilities instead of expending every effort on making this bear dance? Andrei
Oct 16 2009
next sibling parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 Rats, I meant assert(old.gun(i * i)). That's what compounds the
 difficulty of the example.

That wouldn't be allowed. More specifically 'old(gun(i * i))' wouldn't be allowed. 'old(this).gun(i * i)' would be allowed, but probably wouldn't do what you want it to do. 'old(this.clone()).gun(i * i)' would be allowed and would work, assuming that the 'clone' method is defined and has the right semantics. The general rule is that for any 'old(expr)', 'expr' only has access to variables that are accessible in the 'in' block. Preferably const access.
 I honestly believe the whole "old" thing can't be made to work. Shall we
 move on to other possibilities instead of expending every effort on
 making this bear dance?

It definitely /can/ be made to work, for some value of "work". It sacrifices the natural order of evaluation to gain a concise and intuitive syntax. I don't think it should be dismissed out of hand. -- Rainer Deyke - rainerd eldwood.com
Oct 16 2009
parent reply Rainer Deyke <rainerd eldwood.com> writes:
Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 I honestly believe the whole "old" thing can't be made to work. Shall we
 move on to other possibilities instead of expending every effort on
 making this bear dance?

It definitely /can/ be made to work, for some value of "work". It sacrifices the natural order of evaluation to gain a concise and intuitive syntax. I don't think it should be dismissed out of hand.

Also, from the Eiffel docs (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html): The notation 'old expression' is only valid in a routine postcondition. It denotes the value the expression had on routine entry. It seems that Eiffel had 'old' semantics that I've proposed all along. Any significant problems with this approach would have been discovered by the Eiffel community by now. -- Rainer Deyke - rainerd eldwood.com
Oct 17 2009
next sibling parent reply Christopher Wright <dhasenan gmail.com> writes:
Rainer Deyke wrote:
 Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 I honestly believe the whole "old" thing can't be made to work. Shall we
 move on to other possibilities instead of expending every effort on
 making this bear dance?

sacrifices the natural order of evaluation to gain a concise and intuitive syntax. I don't think it should be dismissed out of hand.

Also, from the Eiffel docs (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html): The notation 'old expression' is only valid in a routine postcondition. It denotes the value the expression had on routine entry. It seems that Eiffel had 'old' semantics that I've proposed all along. Any significant problems with this approach would have been discovered by the Eiffel community by now.

It requires duplicating the object. If the object is mutable, this requires duplicating it and recursively duplicating everything it references. If the object is immutable, this is free.
Oct 17 2009
parent reply Rainer Deyke <rainerd eldwood.com> writes:
Christopher Wright wrote:
 Rainer Deyke wrote:
 It seems that Eiffel had 'old' semantics that I've proposed all along.
 Any significant problems with this approach would have been discovered
 by the Eiffel community by now.

It requires duplicating the object. If the object is mutable, this requires duplicating it and recursively duplicating everything it references. If the object is immutable, this is free.

There is no "the object". void f(string fname) out { file_size(fname) >= old(file_size(fname)); } -- Rainer Deyke - rainerd eldwood.com
Oct 17 2009
parent Rainer Deyke <rainerd eldwood.com> writes:
Leandro Lucarella wrote:
 Rainer Deyke, el 17 de octubre a las 14:24 me escribiste:
 There is no "the object".

void f(SomeObjectWithLotsOfReferences obj) out { assert(old(obj).some_check()); }

If 'obj' is a reference type and the reference itself wasn't modified, then 'old(obj)' is the same as 'obj'. Objects are only copied if you explicitly copy them. 'old(x)' means "the cached value of evaluating 'x' at the beginning of the routine". No more, no less. -- Rainer Deyke - rainerd eldwood.com
Oct 17 2009
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Rainer Deyke wrote:
 Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 I honestly believe the whole "old" thing can't be made to work. Shall we
 move on to other possibilities instead of expending every effort on
 making this bear dance?

sacrifices the natural order of evaluation to gain a concise and intuitive syntax. I don't think it should be dismissed out of hand.

Also, from the Eiffel docs (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html): The notation 'old expression' is only valid in a routine postcondition. It denotes the value the expression had on routine entry. It seems that Eiffel had 'old' semantics that I've proposed all along.

Great. Others brought it up too, inspired from Eiffel.
 Any significant problems with this approach would have been discovered
 by the Eiffel community by now.

There is no problem if a copy of the object is made upon entry in the procedure. That's what I think Eiffel does. I was hoping to avoid that by allowing the "out" contract to see the definitions in the "in" contract. Andrei
Oct 17 2009
parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 Rainer Deyke wrote:
 Also, from the Eiffel docs
 (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html):

   The notation 'old  expression' is only valid in a routine
 postcondition. It denotes the value the expression had on routine entry.

 It seems that Eiffel had 'old' semantics that I've proposed all along.

Great. Others brought it up too, inspired from Eiffel.
 Any significant problems with this approach would have been discovered
 by the Eiffel community by now.

There is no problem if a copy of the object is made upon entry in the procedure. That's what I think Eiffel does. I was hoping to avoid that by allowing the "out" contract to see the definitions in the "in" contract.

Copying the object would be completely broken, so I'm sure that that's *not* how Eiffel does it. "It denotes the value the expression had on routine entry." In other words, the expression is evaluated once, on routine entry, and the result is cached for use in the postcondition. -- Rainer Deyke - rainerd eldwood.com
Oct 17 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 Rainer Deyke wrote:
 Also, from the Eiffel docs
 (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html):

   The notation 'old  expression' is only valid in a routine
 postcondition. It denotes the value the expression had on routine entry.

 It seems that Eiffel had 'old' semantics that I've proposed all along.

 Any significant problems with this approach would have been discovered
 by the Eiffel community by now.

procedure. That's what I think Eiffel does. I was hoping to avoid that by allowing the "out" contract to see the definitions in the "in" contract.

Copying the object would be completely broken, so I'm sure that that's *not* how Eiffel does it. "It denotes the value the expression had on routine entry." In other words, the expression is evaluated once, on routine entry, and the result is cached for use in the postcondition.

What if the expression is conditioned by the new state of the object? Andrei
Oct 17 2009
parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 Rainer Deyke wrote:
 Copying the object would be completely broken, so I'm sure that that's
 *not* how Eiffel does it.  "It denotes the value the expression had on
 routine entry."  In other words, the expression is evaluated once, on
 routine entry, and the result is cached for use in the postcondition.

What if the expression is conditioned by the new state of the object?

Not allowed. Since 'old(x)' is the value of 'x' evaluated at the beginning of the function, it must be possible to evaluate 'x' at the beginning of the function. Either rewrite the assertion or drop it. I have a feeling that this will only rarely be an issue. -- Rainer Deyke - rainerd eldwood.com
Oct 17 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 Rainer Deyke wrote:
 Copying the object would be completely broken, so I'm sure that that's
 *not* how Eiffel does it.  "It denotes the value the expression had on
 routine entry."  In other words, the expression is evaluated once, on
 routine entry, and the result is cached for use in the postcondition.


Not allowed. Since 'old(x)' is the value of 'x' evaluated at the beginning of the function, it must be possible to evaluate 'x' at the beginning of the function. Either rewrite the assertion or drop it. I have a feeling that this will only rarely be an issue.

If x is a complex expression and part of a complex control flow, it becomes highly difficult what it means "at the beginning of the function". It also becomes difficult to find a way to distinguish good cases from bad cases without being overly conservative. I have no idea how Eiffel pulls it off. Andrei
Oct 17 2009
parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 If x is a complex expression and part of a complex control flow, it
 becomes highly difficult what it means "at the beginning of the
 function". It also becomes difficult to find a way to distinguish good
 cases from bad cases without being overly conservative.

It looks like a more or less straightforward AST transformation to me. in { } body { F(); } out { G(old(x)); } => { auto old_x = x; try { F(); } finally { G(old_x); } } Repeat for each instance of 'old', in order of appearance. OK, it's not entirely trivial, but it's not prohibitively difficult either. -- Rainer Deyke - rainerd eldwood.com
Oct 17 2009
next sibling parent Rainer Deyke <rainerd eldwood.com> writes:
Rainer Deyke wrote:
  {
    auto old_x = x;
    try {
      F();
    } finally {
      G(old_x);
    }
  }

Not 'finally', unless postconditions are checked when the function terminates with an exception. This is closer to correct: { auto old_x = x; // Preconditions go here. F(); // <-- function body G(old_x); // <-- postcondition } -- Rainer Deyke - rainerd eldwood.com
Oct 17 2009
prev sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 If x is a complex expression and part of a complex control flow, it
 becomes highly difficult what it means "at the beginning of the
 function". It also becomes difficult to find a way to distinguish good
 cases from bad cases without being overly conservative.

It looks like a more or less straightforward AST transformation to me. in { } body { F(); } out { G(old(x)); } => { auto old_x = x; try { F(); } finally { G(old_x); } } Repeat for each instance of 'old', in order of appearance. OK, it's not entirely trivial, but it's not prohibitively difficult either.

It is if x is an _arbitrarily complex_ expression, and if that expression is part of a _complex control flow_. The language definition would have to decide exactly where complex is too complex in the expression or the control flow. That complicates the language. Also, by necessity the feature will be limited and will not give people enough freedom. It's lose-lose. Andrei
Oct 17 2009
parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 It is if x is an _arbitrarily complex_ expression, and if that
 expression is part of a _complex control flow_. The language definition
 would have to decide exactly where complex is too complex in the
 expression or the control flow. That complicates the language. Also, by
 necessity the feature will be limited and will not give people enough
 freedom. It's lose-lose.

The complexity of the expression is irrelevant, since the expression is simply moved to the beginning of the function as a unit. Complex expressions are just simple expressions applied recursively. The compiler already knows how to deal with complex expressions. Control flow is also irrelevant because it is simply ignored. The AST transformation sees this: blah blah old(x) blah old(y) blah ..and turns it into this: blah blah cached_value_0 blah cached_value_1 blah Yes, this means that the expressions 'x' and 'y' cannot use any local variables from the postcondition block. If you want to cache values in the precondition block for use in the postcondition block, you can't wait until you reach the postcondition block before deciding what to cache. This limitation exists whether the caching is manual or automated. If you insist on arguing about this, please direct your complaints to the Eiffel community and tell *them* how the language feature they've been using for years is broken. If there really is something wrong with Eiffel-style 'old' expressions, I'm sure the Eiffel community would know about it. -- Rainer Deyke - rainerd eldwood.com
Oct 17 2009
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
Rainer Deyke wrote:
 Andrei Alexandrescu wrote:
 It is if x is an _arbitrarily complex_ expression, and if that
 expression is part of a _complex control flow_. The language definition
 would have to decide exactly where complex is too complex in the
 expression or the control flow. That complicates the language. Also, by
 necessity the feature will be limited and will not give people enough
 freedom. It's lose-lose.

The complexity of the expression is irrelevant, since the expression is simply moved to the beginning of the function as a unit.

The expression may mutate stuff.
 Complex
 expressions are just simple expressions applied recursively.  The
 compiler already knows how to deal with complex expressions.

Heh, that's not what I was worried about. It's mutation and dependencies.
 Control flow is also irrelevant because it is simply ignored.  The AST
 transformation sees this:
   blah blah old(x) blah old(y) blah
 ..and turns it into this:
   blah blah cached_value_0 blah cached_value_1 blah
 
 Yes, this means that the expressions 'x' and 'y' cannot use any local
 variables from the postcondition block.  If you want to cache values in
 the precondition block for use in the postcondition block, you can't
 wait until you reach the postcondition block before deciding what to
 cache.  This limitation exists whether the caching is manual or automated.
 
 If you insist on arguing about this, please direct your complaints to
 the Eiffel community and tell *them* how the language feature they've
 been using for years is broken.  If there really is something wrong with
 Eiffel-style 'old' expressions, I'm sure the Eiffel community would know
 about it.

If you know about Eiffel's old, I'd appreciate if you explained how it works. I am arguing exactly because I don't know. My understanding is that neither of us currently knows how it works, so I don't think it's ok to refer me to Eiffel. Andrei
Oct 17 2009
parent reply Rainer Deyke <rainerd eldwood.com> writes:
Andrei Alexandrescu wrote:
 Rainer Deyke wrote:
 The expression may mutate stuff.

It shouldn't. It's an error if it does, just like it's an error for an assertion or post/precondition to have any side effects. It would be nice if the compiler could catch this error, but failing that, 'old' expressions are still no worse than assertions in this respect.
 If you know about Eiffel's old, I'd appreciate if you explained how it
 works. I am arguing exactly because I don't know. My understanding is
 that neither of us currently knows how it works, so I don't think it's
 ok to refer me to Eiffel.

My suggestion to ask the Eiffel community directly was meant seriously. -- Rainer Deyke - rainerd eldwood.com
Oct 18 2009
parent reply Michel Fortin <michel.fortin michelf.com> writes:
On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer" 
<schveiguy yahoo.com> said:

 Incidentally, shouldn't all access to the object in the in contract be  
 const by default anyways?

Hum, access to everything (including global variables, arguments), not just the object, should be const in a contract. That might be harder to implement though. -- Michel Fortin michel.fortin michelf.com http://michelf.com/
Oct 20 2009
parent reply Michel Fortin <michel.fortin michelf.com> writes:
On 2009-10-20 11:44:00 -0400, "Steven Schveighoffer" 
<schveiguy yahoo.com> said:

 On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin  
 <michel.fortin michelf.com> wrote:
 
 On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer"  
 <schveiguy yahoo.com> said:
 
 Incidentally, shouldn't all access to the object in the in contract be  
  const by default anyways?

Hum, access to everything (including global variables, arguments), not just the object, should be const in a contract. That might be harder to implement though.

Yeah, you are probably right. Of course, a const function can still alter global state, but if you strictly disallowed altering global state, we are left with only pure functions (and I think that's a little harsh).

Not exactly. Pure functions can't even read global state (so their result can't depend on anything but their arguments), but it makes perfect sense to read global state in a contract. What you really need is to have a const view of the global state. And this could apply to all asserts too. -- Michel Fortin michel.fortin michelf.com http://michelf.com/
Oct 20 2009
parent reply Michel Fortin <michel.fortin michelf.com> writes:
On 2009-10-20 12:04:20 -0400, "Steven Schveighoffer" 
<schveiguy yahoo.com> said:

 On Tue, 20 Oct 2009 11:57:05 -0400, Michel Fortin  
 <michel.fortin michelf.com> wrote:
 
 On 2009-10-20 11:44:00 -0400, "Steven Schveighoffer"  
 <schveiguy yahoo.com> said:
 
 On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin   
 <michel.fortin michelf.com> wrote:
 
 On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer"   
 <schveiguy yahoo.com> said:
 
 Incidentally, shouldn't all access to the object in the in contract  be 
   const by default anyways?

not just the object, should be const in a contract. That might be harder to implement though.

alter global state, but if you strictly disallowed altering global state, we are left with only pure functions (and I think that's a little harsh).

Not exactly. Pure functions can't even read global state (so their result can't depend on anything but their arguments), but it makes perfect sense to read global state in a contract. What you really need is to have a const view of the global state. And this could apply to all asserts too.

Yes, but what I'm talking about is "what functions can you call while in a contract." Access to data should be const as you say. But if you follow that logic to the most strict interpretation, the only "safe" functions to allow are pure functions. i.e.: int x; class C { void foo() in { x = 5; // I agree this should be an error bar(); // ok? } {} void bar() const { x = 5; } }

When you try to write to x yes it's an error. But if you were reading x it should not be an error. Basically inside the contract a global like x should be seen as const(int) just like the object should be seen as const(C). Pure functions are somewhat alike, but are more restrictive since you can only access immutable globals. So what we need is semi-pure functions that can see all the globals as const data, or in other terms having no side effect but which can be affected by their environment. Another function qualifier, isn't it great! :-) -- Michel Fortin michel.fortin michelf.com http://michelf.com/
Oct 20 2009
parent =?UTF-8?B?IkrDqXLDtG1lIE0uIEJlcmdlciI=?= <jeberger free.fr> writes:
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: quoted-printable

Steven Schveighoffer wrote:
 On Tue, 20 Oct 2009 13:13:07 -0400, Michel Fortin=20
 <michel.fortin michelf.com> wrote:
=20
 So what we need is semi-pure functions that can see all the globals as=


 const data, or in other terms having no side effect but which can be=20
 affected by their environment. Another function qualifier, isn't it=20
 great! :-)

Yeah, I meant which functions to allow among the functions types we=20 already have. To introduce another function type *just to allow=20 contracts to call them* is insanity. =20

function in C/C++: __attribute__((const)) Jerome --=20 mailto:jeberger free.fr http://jeberger.free.fr Jabber: jeberger jabber.fr
Oct 20 2009
prev sibling parent "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Tue, 20 Oct 2009 13:13:07 -0400, Michel Fortin  
<michel.fortin michelf.com> wrote:

 So what we need is semi-pure functions that can see all the globals as  
 const data, or in other terms having no side effect but which can be  
 affected by their environment. Another function qualifier, isn't it  
 great! :-)

Yeah, I meant which functions to allow among the functions types we already have. To introduce another function type *just to allow contracts to call them* is insanity. -Steve
Oct 20 2009
prev sibling parent "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Tue, 20 Oct 2009 11:57:05 -0400, Michel Fortin  
<michel.fortin michelf.com> wrote:

 On 2009-10-20 11:44:00 -0400, "Steven Schveighoffer"  
 <schveiguy yahoo.com> said:

 On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin   
 <michel.fortin michelf.com> wrote:

 On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer"   
 <schveiguy yahoo.com> said:

 Incidentally, shouldn't all access to the object in the in contract  
 be   const by default anyways?

not just the object, should be const in a contract. That might be harder to implement though.

alter global state, but if you strictly disallowed altering global state, we are left with only pure functions (and I think that's a little harsh).

Not exactly. Pure functions can't even read global state (so their result can't depend on anything but their arguments), but it makes perfect sense to read global state in a contract. What you really need is to have a const view of the global state. And this could apply to all asserts too.

Yes, but what I'm talking about is "what functions can you call while in a contract." Access to data should be const as you say. But if you follow that logic to the most strict interpretation, the only "safe" functions to allow are pure functions. i.e.: int x; class C { void foo() in { x = 5; // I agree this should be an error bar(); // ok? } {} void bar() const { x = 5; } } -Steve
Oct 20 2009
prev sibling next sibling parent "Denis Koroskin" <2korden gmail.com> writes:
On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu  
<SeeWebsiteForEmail erdani.org> wrote:

 Jason House wrote:
 if fun or gun is impure, then they should not be callable by the
 contracts. Because of that, order is irrelevant.

1. Restricting calls to pure functions is sensible, but was deemed too restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei

When not just let users one variable of type Variant per contract to store whatever they want?
Oct 16 2009
prev sibling next sibling parent "Denis Koroskin" <2korden gmail.com> writes:
On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2korden gmail.com>  
wrote:

 On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu  
 <SeeWebsiteForEmail erdani.org> wrote:

 Jason House wrote:
 if fun or gun is impure, then they should not be callable by the
 contracts. Because of that, order is irrelevant.

1. Restricting calls to pure functions is sensible, but was deemed too restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei

When not just let users one variable of type Variant per contract to store whatever they want?

I mean, not a Variant, but a Dynamic* object so that the following would be possible: void push(T)(T val) in(storage) { storage.oldSize = this.size; // store //storage.anyDynamicProperty = anyDynamicValue; in general case } out(storage) { assert(storage.oldSize + 1 == this.size); // access } body { // impl } *do you recall the Dynamic class discussion (a class that allows any arbitrary methods and properties access, similar to JavaScript objects or dynamic objects in C#)
Oct 16 2009
prev sibling next sibling parent "Denis Koroskin" <2korden gmail.com> writes:
On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2korden gmail.com>  
wrote:

 On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2korden gmail.com>  
 wrote:

 On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu  
 <SeeWebsiteForEmail erdani.org> wrote:

 Jason House wrote:
 if fun or gun is impure, then they should not be callable by the
 contracts. Because of that, order is irrelevant.

1. Restricting calls to pure functions is sensible, but was deemed too restrictive. 2. Even so, there's difficulty on what to cache. The amount cached may depend on both the old and new object (in my example it only depends on the old object). 3. There's too much hidden work and too much smarts involved. I just don't think that's a feasible solution with what we know and have right now. Andrei

When not just let users one variable of type Variant per contract to store whatever they want?

I mean, not a Variant, but a Dynamic* object so that the following would be possible: void push(T)(T val) in(storage) { storage.oldSize = this.size; // store //storage.anyDynamicProperty = anyDynamicValue; in general case } out(storage) { assert(storage.oldSize + 1 == this.size); // access } body { // impl } *do you recall the Dynamic class discussion (a class that allows any arbitrary methods and properties access, similar to JavaScript objects or dynamic objects in C#)

On second thought Dynamic objects need run-time reflection that D currently lacks. Alternatively users may be given a Variant[string] assoc.array as a poor-man's replacement for a full-fledged Dynamic object: void push(T)(T val) in(storage) { storage["oldSize"] = this.size(); } out(storage) { assert(*storage["oldSize"].peek!(int) == this.size - 1); } body { // impl } The contracts userdata would be stored in a stack alongside with monitor, classinfo etc for classes, and past the data fields for structs.
Oct 16 2009
prev sibling next sibling parent "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Sun, 18 Oct 2009 03:44:39 -0400, Rainer Deyke <rainerd eldwood.com>  
wrote:

 Andrei Alexandrescu wrote:
 Rainer Deyke wrote:
 The expression may mutate stuff.

It shouldn't. It's an error if it does, just like it's an error for an assertion or post/precondition to have any side effects. It would be nice if the compiler could catch this error, but failing that, 'old' expressions are still no worse than assertions in this respect.

I'm coming into this a little late, but what Rainer is saying makes sense to me. Would it help to force any access to the object to be treated as if the object is const? i.e.: old(this.x) would be interpreted as: (cast(const(typeof(this))this).x and cached in the input contract section. It seems straightforward that Rainer's solution eliminates the boilerplate code of caching values available in the in contract, and if you force const access, prevents calling functions which might mutate the state of the object. But it uses the correct contract -- this object is not mutable for this call only. I agree pure is too restrictive, because then the object must be immutable, no? Incidentally, shouldn't all access to the object in the in contract be const by default anyways? -Steve
Oct 20 2009
prev sibling parent "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Tue, 20 Oct 2009 08:36:14 -0400, Michel Fortin  
<michel.fortin michelf.com> wrote:

 On 2009-10-20 08:16:01 -0400, "Steven Schveighoffer"  
 <schveiguy yahoo.com> said:

 Incidentally, shouldn't all access to the object in the in contract be   
 const by default anyways?

Hum, access to everything (including global variables, arguments), not just the object, should be const in a contract. That might be harder to implement though.

Yeah, you are probably right. Of course, a const function can still alter global state, but if you strictly disallowed altering global state, we are left with only pure functions (and I think that's a little harsh). -Steve
Oct 20 2009
prev sibling next sibling parent reply Kagamin <spam here.lot> writes:
Andrei Alexandrescu Wrote:

     void push(T value);
     in {
        auto oldLength = length();
     }
     out {
        assert(value == top());
        assert(length == oldLength + 1);
     }
 
 Walter tried to implement that but it turned out to be very difficult
 implementation-wise.

What is the problem? Syntactical, semantical or ABI-related?
Oct 15 2009
parent Ary Borenszweig <ary esperanto.org.ar> writes:
Kagamin wrote:
 Andrei Alexandrescu Wrote:
 
     void push(T value);
     in {
        auto oldLength = length();
     }
     out {
        assert(value == top());
        assert(length == oldLength + 1);
     }

 Walter tried to implement that but it turned out to be very difficult
 implementation-wise.

What is the problem? Syntactical, semantical or ABI-related?

This. What does it mean "implementation-wise"?
Oct 15 2009
prev sibling next sibling parent MIURA Masahiro <echochamber gmail.com> writes:
Andrei Alexandrescu wrote:
    void push(T value);
    in {
       auto oldLength = length();
    }
    out {
       assert(value == top());
       assert(length == oldLength + 1);
    }

Another keyword abuse: void push(T value); in { auto in.oldLength = length(); } out { assert(value == top()); assert(length == in.oldLength + 1); }
Oct 15 2009
prev sibling parent Leandro Lucarella <llucax gmail.com> writes:
Rainer Deyke, el 17 de octubre a las 14:24 me escribiste:
 Christopher Wright wrote:
 Rainer Deyke wrote:
 It seems that Eiffel had 'old' semantics that I've proposed all along.
 Any significant problems with this approach would have been discovered
 by the Eiffel community by now.

It requires duplicating the object. If the object is mutable, this requires duplicating it and recursively duplicating everything it references. If the object is immutable, this is free.

There is no "the object". void f(string fname) out { file_size(fname) >= old(file_size(fname)); }

There is an object if you have this: void f(SomeObjectWithLotsOfReferences obj) out { assert(old(obj).some_check()); } But I don't see why the only option is too recursively copy the entire object. You can do a shallow copy too. It's a little more error prone since the programmer need to ensure that all needed "old" references are kept, but it's realistic. And you have the exact same problem with the ugly-nasty-oh-please-don't-do-it-like-that associative array of variant approach too =) So, if you *really* think that this "old stuff" is needed for contracts, I prefer the old() approach than the ugly-nasty-...-that associative array of variant =P -- Leandro Lucarella (AKA luca) http://llucax.com.ar/ ---------------------------------------------------------------------- GPG Key: 5F5A8D05 (F8CD F9A7 BF00 5431 4145 104C 949E BFB6 5F5A 8D05) ---------------------------------------------------------------------- Me encanta el éxito; por eso prefiero el estado de progreso constante, con la meta al frente y no atrás. -- Ricardo Vaporeso. Punta del Este, Enero de 1918.
Oct 17 2009