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.

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