|
|
Meine Frage:
Hi hab mal eine Aufgabe wo ich gerade nicht weiterkomme.
Gegeben sei folgendes Programmfragment in Form einer Beweisskizze, also mit eingefu?gten Zusicherungen Pre, Inv und Post:
{Pre}
{Inv}
while(z<x){
{Inv}
z=z+1;
y=y+z;
}
{post}
Es gilt:
Pre(Vorbedingung) = (x >= 0) und (y = 0) und (z = 0)
Inv(Invariante)= (z<=x) und (y= z(z+1)/2)
Post(Nachbedingung)= (y= x(x+1)/2)
Finden Sie eine gemäß Vorlesung geeignete Funktion f und beweisen Sie mit ihr die Terminierung der Schleife.
Ich weiß nicht wie ich bei dieser Aufgabe vorgehen soll.
Meine Ideen:
Als 1. soll ich zeigen wie die Schleife terminiert. while(z<x) ist ja dass die Schleife irgendwann enden muss.
Jedoch wie gehe ich am besten vor um eine Funktion f aufzustellen?
da die Schleifenbedingung (z<x) ist und z inkrementiert würde ich sagen dass die funktion streng monoton steigend ist.
Das ist ja aber noch kein Beweis.
Also meine Frage ist, wie komme ich da drauf...
Danke schonmal im Vorraus
|
|
habs übersehen