Communicating between in and out contracts

[Kagamin]

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