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