• Kagamin <spam here.lot> Oct 15 2009

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