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