On Tuesday, 21 June 2022 at 07:26:50 UTC, Ola Fosheim Grøstad wrote: > If you specify preconditions/postconditions then the exit check > should be considered part of the assumed precondition and the > asserted postcondition. The «exit check» that is the class invariant.