On 12/13/2012 12:43 AM, Walter Bright wrote:
On 12/12/2012 3:23 PM, Timon Gehr wrote:
It is somewhat similar to (the still quite broken) 'pure' in D,
Broken how?
- There is no way to specify that a delegate is strongly pure without
resorting to type deduction, because
- Member functions/local functions are handled inconsistently.
- Delegate types legally obtained from certain member functions are
illegal to declare.
- 'pure' means 'weakly pure' for member functions and 'strongly
pure' for local functions. Therefore it means 'weakly pure' for
delegates, as those can be obtained from both.
- Delegates may break the transitivity of immutable, and by extension,
shared.
A good first step in fixing up immutable/shared would be to make
everything that is annotated 'error' pass, and the line annotated 'ok'
should fail:
import std.stdio;
struct S{
int x;
int foo()pure{
return x++;
}
int bar()immutable pure{
// return x++; // error
return 2;
}
}
int delegate()pure s(){
int x;
int foo()pure{
// return x++; // error
return 2;
}
/+int bar()immutable pure{ // error
return 2;
}+/
return &foo;
}
void main(){
S s;
int delegate()pure dg = &s.foo;
// int delegate()pure immutable dg2 = &s.bar; // error
writeln(dg(), dg(), dg(), dg()); // 0123
immutable int delegate()pure dg3 = dg; // ok
writeln(dg3(), dg3(), dg3(), dg3()); // 4567
// static assert(is(typeof(cast()dg3)==int delegate() immutable pure));
// error
auto bar = &s.bar;
pragma(msg, typeof(bar)); // "int delegate() immutable pure"
}
Provided the code is correct.
No language or compiler can prove code correct.
Sometimes it can. Certainly a compiler can check a user-provided proof.
eg: http://coq.inria.fr/
A minor issue with proving code correct is of course that the proven
specification might contain an error. The formal specification is often
far more explicit and easier to verify manually than the program though.
