lösung Beweis Induktion Algorithmus beweise

Beweis eines Algorithmus mnittels Induktion

Hi,

hab ein ziemlich großes Problem. Ich muß einen Algorithmus, bzw. einen Teil davon mittels Induktion beweisen. Mathematisch gesehen, kann ich eine Induktion, das find ich auch nicht so schwer...
Aber jetzt das ganze in meinen Algorithmus zu transportieren, ich weiß nicht, irgendwo fehlt mir da die Vorstellung; erbitte also ganz dringend Hilfe: mich interessiert nicht so sehr die Lösung, sondern viel mehr, wie ich die einzelnen Schritte erbringe.
So, und hier ist das gute Stück:

Beweise für den folgenden Algorithmus die Invariante I2 mittels Induktion.
Eingabe:
a € N0, b € N0 (also Element N Null)
Ausgabe:
c € N0: c = a * b
Hilfsvariablen:
i € N0, j € N0

Berechnung:
01 c ← 0
02 i ← 0
03 solange i < a tue:
04 // Hier gilt die Invariante I1: c = i * b
05 j ← 0
06 solange j < b tue:
07 // Hier gilt die Invariante I2: c = i * b + j
08 c ← c + 1
09 j ← j + 1
10 i ← i + 1

Ich habe mir dazu folgendes überlegt:

Induktion über i € N0
Für ein beliebiges (aber konstantes) i € N gilt beim Schleifentest
(j < b):
c € N0

Mit j < b wird die Verzweigung betreten, die Zuweisungen ausgeführt und es gilt:
j = i

Nach der Verzweigung gilt somit:
j = {0,...,i}

Nach der Ausführung von i = i + 1 und damit für den nächsten Schleifentest gilt:
j = {0,...,i-1}

Sind die Gedanken schon mal zu gebrauchen oder lieg ich völlig falsch. Wie muß ich denn dann rechnen?

Für eine ausführliche Erklärung wär ich echt super dankbar!!!

sagt der Equus