Contracts, Undefined Behavior, and Defensive,Programming

[Timon Gehr]

On 14.06.20 14:49, Mark wrote:
> 
> "guaranteed postconditions", for lack of a better expression.

Or more generally, it would actually be useful to have multiple pairs of 
pre- and postconditions, where each postcondition is established iff the 
corresponding precondition is established. This would also give a more 
natural way to inherit contracts. Your "guaranteed postcondition" would 
be a pre-/postcondition pair where the precondition is `true`.

> In other words, invoking sort with an invalid comparator might mess up 
> the given vector, but at least no "catastrophes" occur. Luckily, in D we 
> have attributes (pure, @safe, nothrow) that basically impose such useful 
> "guaranteed postconditions" and are mechanically checkable.

I wish. Right now, a failing assertion causes _language_ UB, even though 
assertions are allowed in @safe code. It's a hole in the mechanical 
checking.