On Friday, 3 October 2014 at 17:40:43 UTC, Sean Kelly wrote:
A contract has preconditions and postconditions to validate different types of errors. Preconditions validate user input (caller error), and postconditions validate resulting state (callee error).
Technically, a precondition validates correct argument passing from "caller", which is not quite the same as "user input". "User" in this context is really the "end user", and is *not* what contracts are made for.
Also, I don't think "postconditions" are meant to check "callee" errors. That's what asserts do. Rather, postconditions are verifications that can ony occur *after* the call. For example, a function that takes an input range (no length), but says "input range shall have exactly this amount of items..." or "input shall be no bigger than some unknown value, which will cause a result overflow".
