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