Post

Code contract invariants are poorly named. Should be "pre and post assertion". Something about the word invariant implies no-change.