Comment #0 by bearophile_hugs — 2010-02-26T13:49:46Z
Currently preconditions and postconditions (D contract based programming) can modify input arguments, this prints [0, 2]:
import std.stdio: writeln;
void foo(int[] arr)
out { arr[0] = 0; }
body {}
void main() {
auto a = [1, 2];
foo(a);
writeln(a);
}
But I think it's better if arguments are seen as const inside preconditions and postconditions. Because modifying them alters too much the program behaviour between release and not release builds.
And I think it's better if instance/static attributes are seen as const inside class/struct invariants:
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);
}
That code prints different things if compiled in release or not release mode.
----------------------
A small syntactic related problem:
This is correct syntax:
out{}
out(return){}
invariant(){}
This is not valid syntax:
out(){}
invariant{}
I suggest to make such syntax more uniform to help the programmer.
A permissive solution is to allow the following syntax too:
out(){}
invariant{}
Otherwise the syntax:
invariant(){}
Can become, for symmetry with "out":
invariant{}
Comment #1 by bearophile_hugs — 2010-03-01T09:09:00Z
In practice pre/post conditions and invariants can even become pure. This limits some of their usages (logging, printing), but not much.
Generally reading and modifying a global variable inside a condition/invariant doesn't look like tidy code.
Comment #2 by andrej.mitrovich — 2010-08-30T06:10:35Z
(In reply to comment #0)
> Currently preconditions and postconditions (D contract based programming) can
> modify input arguments, this prints [0, 2]:
>
> import std.stdio: writeln;
>
> void foo(int[] arr)
> out { arr[0] = 0; }
> body {}
>
> void main() {
> auto a = [1, 2];
> foo(a);
> writeln(a);
> }
>
> But I think it's better if arguments are seen as const inside preconditions and
> postconditions. Because modifying them alters too much the program behaviour
> between release and not release builds.
>
Yes. As stated in TDPL, changing the state of the application inside an in/out contract is *illegal*. An application must run with the same behavior and results whether or not it executes it's contracts (debug vs release mode).
I'm not sure about invariants. Although it would be best if they didn't modify the state of 'this', they are still allowed to call private methods and in turn those methods might change the state of the application.
Comment #3 by bearophile_hugs — 2010-10-02T04:30:04Z
See also bug 4974
Comment #4 by robert.schadek — 2024-12-13T17:51:28Z