Um processo P, com entradas i1, i2, i3 e saída o1 é descrito pelas seguintes pré e pós-condições:
Pré : \( \{ i_1\ge 0, i_2\ge 0, i_3\ge 0\} \)
Pós: \( \{(( o_1 \ge i_1) ∧ (o_1 \ge i_2) ∧ (o_1 \ge i_3)) \)
\( ∧ \)
\( ((o_1 = i_1) ∨ (o_1 = i_2) ∨ (o_1 = i_3))\} \)
A função executada pelo processo P produz como saída:
