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
