See DBC but in summary:

1. State the preconditions, i.e. what has to true before operation
2. Describe operation
3. If the preconditions were met, we promise the postcondition is met.

pre: { x >= 0 }
calculate y which is the sqrt(x)
post: { y * y = x and y >= 0 }