postconditions

Output type and side effects of a function.