Suche Schleifeninvariante

Algorithmus 2 mit der Eingabe x, a element N

result = 1
current = x
while a > 0 do
if a ungerade then
result = result * current
end if
current = current * current
a = a/2
end while

return result

also ich weiß das der algorithmus x^a berechnet…
aber wie kann ich das jetzt am besten mit einer schleifeninvariante beweiesen

danke für eventuelle hilfe

Schreibfehler?
Da ist sicherlich was nicht korrekt abgeschrieben, da das Programm loopt und nur in Abhängigkeit der konkreten Implementierung terminiert.
Für a > 0 wird a in der Schleife halbiert. Doch ein a größer 0 bleibt bei einer Division weiterhin größer 0. Nur wenn der Wert aus der Range des Datentyps fällt, wird wahrscheinlich 0 als Resultat gesetzt.

Also nochmal schauen, ob die Operation mit a stimmen.

Ciao, Allesquatsch

nein das stimmt so
ich dachte das am anfang auch, aber a und x sind element der nat. zahlen
also ganzzahlige division, d.h. es wird zwangsläufig 0

Hallo,

also ich weiß das der algorithmus x^a berechnet…
aber wie kann ich das jetzt am besten mit einer
schleifeninvariante beweiesen

Als Invariante kannst du wählen:

result * current^a

Vor dem ersten Schleifendurchlauf ist das einfach x^a, also das Eregebnis.

Jetzt musst du nur noch beweisen, dass result * current^a auch nach jeder Iteration noch den gleichen Wert hat.

Grüße,
Moritz