"Before and after" in contracts?

[bearophile]

spir:

> Contracts, like any software tool, do not correctly match all possibly needs.

This is true in general, but this isn't true in this case: here they don't match a basic need because D DbC misses a significant feature (prestate). If you take a look at other implementations of DbC in Eiffel and C# the prestate is present.

Bye,
bearophile