Like the title says. The post conditions of a routine must be a subset of the preconditions for the routine?

The way I understand post-conditions is that they are entirely independent of preconditions, so my understanding leads me to think that they are not a subset of preconditions.

Any input would be appreciated.

1 Answer 1


How about a concrete example:

int x;
// Preconditions: none (empty set)
// Postconditions: x = y
void assign_to_x(int y) { x = y; }

If you allow any form of mutable state in your program, you can have postconditions that are not subsets of your preconditions.

  • Thank you! That makes it clearer. EDIT: I'm new here, is there an upvote button somewhere?
    – user106857
    Nov 4, 2013 at 18:24
  • @user106857 Click the checkmark beside the answer, it both gives bstamour rep and marks the question as answered Nov 4, 2013 at 18:44
  • +1 Excellent answer. Suggest you expand it to explain more fully.
    – andy256
    Nov 5, 2013 at 3:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.