A question about DbC

[Denis Koroskin]

On Sat, 09 Oct 2010 14:20:18 +0400, Jonathan M Davis <jmdavisProg at 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.