Tidier pre/post conditions
bearophile
bearophileHUGS at lycos.com
Fri Feb 26 14:35:09 PST 2010
Generally a program can produce different outputs between release and not release mode, but I always like to minimize the probability of this.
Two examples:
---------------
import std.stdio: writeln;
void foo(int[] arr)
out { arr[0] = 0; }
body {}
void main() {
auto a = [1, 2];
foo(a);
writeln(a);
}
---------------
import std.stdio: writeln;
struct Foo {
int x;
invariant() { this.x -= 10; }
void incr() { x++; }
}
void main() {
Foo f;
writeln(f.x);
f.incr();
writeln(f.x);
f.incr();
writeln(f.x);
}
---------------
The problem can be reduced if input arguments are seen as const inside pre/post conditions, and attributes are seen as const inside class/struct invariants. This is what I have asked:
http://d.puremagic.com/issues/show_bug.cgi?id=3856
But there's an alternative solution, to let the compiler accept only pure pre/post conditions (and invariants that can only read attributes and write nothing), but I am not sure if this can be a bit too much restrictive (can you invent situations where this is too much restrictive?), so for now I have asked just for the less restrictive thing.
Bye,
bearophile
More information about the Digitalmars-d
mailing list