Korrektheit eines Algorithmus prüfen?

[Mauritio]

Hallo zusammen,

ich bin gerade dabei für eine Klausur (Algorithmen und Datenstrukturen) zu lernen.

Dabei bin ich auf folgende Aufgabe gestoßen:

Gegeben sei folgender Programmabschnitt, der eine natürliche Zahl A in ihre Primfaktoren zerlegt:

k = 0;
i = 2;
while (n > 1) {
if (n % i == 0) {
a[k] = i;
k = k + 1;
n = n / i;
} else {
i = i + 1;
}
}

Weiterhin gegeben ist die Spezifikation:
- Vorbedingung: {n = A >= 1}
- Nachbedingung: {a[0] * a[1] *...* a[k - 1] = A}

Stellen Sie zunächst eine Invariante auf und zeigen Sie dann deren Gültigkeit durch Einfügen von Vor- und Nachbedingungen in den Programmtext.
Hinweis: Es muss nur die Nachbedingung bewiesen werden, nicht, dass die a Primzahlen sind.

Mein Problem ist jetzt, dass ich nicht so ganz verstehe, wie ich hier am besten vorgehe. Eine Invariante beschreibt ja quasi, all diejenigen Programmteile, die sich beim Ausführen des Algorithmus nicht verändern. Ist das in etwas richtig?

Wäre echt nett, wenn mir jemand sagen könnte, wie ich hier am besten vorgehe. Ich will nicht, dass jemand anderes die Aufgabe für mich löst, sondern mir nur Hinweise gibt, die mich weiterbringen könnten!

Vielen Dank!
Mauritio

 

[fastjack]

Whl. sollst Du einen Beweis mit vollständiger Induktion über die eingefügten Nachbedingungen machen.

 

[hartzie]

Da kann ich dir helfen. Hier ein Link wo eine formale Verifikation über Bubblesort gemacht wurde:
http://www.informatik.uni-bremen.de/agbs/lehre/ws0809/pi1/hintergrund/formale_verifikation.pdf
Anhand von diesem Beispiel müsste sich dein kleiner Formalismus leicht beweisen lassen.