# Korrektheit eines Algorithmus prüfen?



## Mauritio (16. Jan 2011)

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:
> 
> 
> ```
> ...


_

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 (17. Jan 2011)

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


----------



## hartzie (17. Jan 2011)

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.


----------

