[justneedaname]

Anyone interested in other languages that implement this should take a look at the SPARK subset of Ada. Pre and postconditions work in the same way and enforce the same behaviour described here (or at least that's what I understand it to do from a quick skim through)

[rwmj]

Wasn't Eiffel the first "design by contract" language? https://en.wikipedia.org/wiki/Eiffel_(programming_language)

[pjmlp]

Yes, with key books based on it.

[bluGill]

The authors are aware of SPARK and are trying to bring that to C++.