Eingabe : natürliche Zahl a, nat. Zahl b.
-- Vorbedingung: a = A und b = B
Rechnung :
Zahl c := 0;
-- Invariante: a * b + c = A * B
solange (b > 0) wiederhole {
c := c + a; b := b - 1;
}
Ausgabe : c. -- Nachbedingung: c = A * B