On 14.06.20 17:14, Timon Gehr wrote: > where each postcondition is established iff the corresponding > precondition is established Typo: That should have been `if`, not `iff`. (Of course the postcondition is allowed to hold even if the corresponding precondition does not.)