On Sat, 09 Oct 2010 14:20:18 +0400, Jonathan M Davis <jmdavisp...@gmx.com>
wrote:
On Saturday 09 October 2010 03:09:30 Denis Koroskin wrote:
Given that pre-, post-conditions and invariants are all pure, it doesn't
really matter in what order they are executed.
In effect yes, but they aren't actually pure. If they were, you couldn't
use stuff
like writeln() in them. However, since they go away in release builds
and aren't
supposed to have any effect on the program (beyond throwing AssertErrors
on
failed assertions), they are in effect pure, so you're essentially
correct. But
still, they aren't actually pure.
- Jonathan M Davis
Well, I meant they are conceptually pure.
But do believe you shouldn't be able to use writeln in code like that. Why
would you do it anyway? It's more or less like using assert just for a
console output:
try {
assert(false, "message");
} catch {
}
Put your logging stuff into the body, not into the contracts.
