Chapter 4:

Postcondition: a condition the implementer guarantees will hold when a method or constructor completes execution

Invariant: a condition that always holds true

Class invariant: an invariant regarding properties of class instances; that is, a condition that will always be true for all instances of a class

If (condition)
Statement

And the if-then-else has the form

If(condition)
Statement1
Else
Statement2