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
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 reply "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
parent reply "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
Oct 16 2009
parent reply "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  



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
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 



 
 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 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



 
 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.


 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



 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?


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:


<snip

 
 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 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 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
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?


 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.


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 reply 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
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".


 There is an object if you have this:
 
 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?


 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.


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.


 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.


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.


 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.


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 "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
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 "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
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 "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?


  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.


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
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?


  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.


 
 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 reply "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
parent =?UTF-8?B?IkrDqXLDtG1lIE0uIEJlcmdlciI=?= <jeberger free.fr> writes:
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=




=20

 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! :-)


=20
 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


	Note that there already is a gcc extension for this kind of=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 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 Kagamin <spam here.lot> writes:
Chris Nicholson-Sauls Wrote:


 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);
      }


We have so many nifty keywords in D, I can't stand against abusing them
(contracts already do it).

     void push(T value);
     shared {
        typeof(length()) oldLength;
     }
     in {
        oldLength = length();
     }
     out {
        assert(value == top());
        assert(length == oldLength + 1);
     }
Oct 15 2009
prev 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