Comment by 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)