Terminieren von Schleifen

Neue Frage »

Auf diesen Beitrag antworten »
georg28 Terminieren von Schleifen

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
 
Auf diesen Beitrag antworten »
Airblader

Es macht keinen Spa?, wenn ? Fragen copy?paste ???? so dass ??? v?llig unleser?ich s?nd.
Auf diesen Beitrag antworten »
georg28

sorry und verbessertsmile habs übersehensmile
 
Neue Frage »
Antworten »


Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »