Disseny iteratiu · 4.2

Correctesa de programes iteratius

Justificar que un bucle fa el que diu: l'invariant es manté, en sortir es compleix la postcondició i el bucle acaba.