3 ms·
A postcondition is an invariant[1]. Invariants must hold at the end of the operation however the intervening inconsistent state must be invisible (effectively,
by _a_a_a_ 3y ago
A postcondition is an invariant[1]. Invariants must hold at the end of the operation however the intervening inconsistent state must be invisible (effectively, be atomic). They often are (maybe always are?) violated within the operation but must be patched up by the end.
[1] Edit: no, a postcondition expresses an invariant in code - but that's a terminology thing. We may be disagreeing just on terminology here.
- rcxdude 3y agoprecondition is something which must be true before some code executes postcondition is something which must be true after some code executes invariant is both: something which must be true both before and after some code executes. So it's the other way around. An invariant is a postcondition, but a postcondition is not necessarily an invariant. (you can check all three with assertions, but they will generally exist whether you check them or not)
- _a_a_a_ 3y agoA reasonable distinction. I accept it.