Communicating between in and out contracts

[Rainer Deyke]

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 at eldwood.com