Terminierung von Schleifen

[Brombeere]

Hallo,

ich habe gleich noch eine Frage:

und zwar ist folgender Programmabschnitt gegeben:

// Es gilt n > 0.
int a = 2;
int b = n;
while (a < b + 10) {
 a = a * 2;
 b = b + 1;
}

In der Schleife wird a immer verdoppelt, b um 1 erhöht. Beweisen soll man nun die Terminierung von Schleifen, streng nach einer Vorgabe der Vorlesung:

Man soll zu den "Iterationen 0,1,... eine Folge von Werten u 0, u1, u2 ..., die sich jeweils nach einer
festen Formel aus den Werten von Programmvariablen ergeben, konstruieren, und zwar für u0 bei Eintritt in die Schleife und für ui am Ende der i-ten Iteration (for: nach Inkrement)
Zum Beweis der Terminierung genügt dann nachzuweisen, dass:
1. u0 > 0
2. u < u - d für alle i und einen festen Wert d > 0
3. Für ui ≤ 0 wird die Schleife nach der i-ten Iteration verlassen".

Um mal direkt die Vorlesung zu zitieren.

Ich hab mir nun folgendes überlegt:

u=b-a+2

1. Für u_0 gilt dann: u=n-2+2=n. Da n>0 ist, u_0 echt größer 0.
2. u_i=b-a+2=n-a+2
u_i+1=b+1-2a+2=n-2a+3
Wenn man das vergleicht und beachtet, dass a>=2 sieht man doch: Für den kleinsten Fall a=2 gilt:
u_i=n-2+2=n; u_i+1=n-4+2=n-2. Für die restlichen Fälle gilt dies ja erst recht: u_i<u_i+1.
3. Damit hab ich Probleme, das z beweisen.

 

[Brombeere]

in 2. soll bewiesen werden: u_i+1<ui - d für alle i und einen festen Wert d > 0

 

[njans]

Das ganze hat sehr wenig mit Java zu tun ist viel mehr reine Mathematik. Wenn deine Fragen immer in diese Richtung schlagen solltest du diese vielleicht in einem Mathe-Forum posten

 

[cmrudolph]

Ich weiß jetzt nicht, wie ihr es formal in eurer Vorlesung macht. Aber ich kenne Terminationsbeweise so, dass man eine monoton fallende Folge finden muss um zu zeigen, dass eine Schleife terminiert.

Mein Ansatz wäre ungefähr so:

Schleifenbedingung umschreiben:
0 < b + 10 - a

f(i) := b + 10 - a
a = 2^i
b = i + n
=> f(i) = i + n - 2^i

z. z.: f(i) ist monoton fallend.

Ansatz: Induktionsbeweis

I. A.: f(0) = n - 1 <= f(1) = 1 + n - 2
I. S.: f(n + 1) = n + 1 + n - 2^(n + 1) = 2n + 1 - 2^n * 2 < 2n + 1 - 2^n < f(n) = 2n - 2^n
q.e.d.

Das erste < steht da, weil n > 0, bei n >= 0 müsste es <= heißen. Würde dem Beweis aber nicht schaden.
Wenn man den Induktionsanfang bei i = 1 startet, kann man zeigen, dass f(i) ab dort streng monoton fallend ist.

Wie das jetzt allerdings in deine Vorlesung passt weiß ich nicht.

 

[Brombeere]

Und wie sieht es mit meinem Ansatz aus?

Gefordert ist eigentlich nur nach dem SChema vorzugehen

1. u0 > 0
2. u_i+1 < u_i - d für alle i und einen festen Wert d > 0
3. Für ui ≤ 0 wird die Schleife nach der i-ten Iteration verlassen".

 

[cmrudolph]

Und wie sieht es mit meinem Ansatz aus?

Ich habe dir jetzt einen Beweis geliefert. Die Resteigenleistung den Beweis in dein Schema zu überführen bleibt dir überlassen. Wenn dir das nicht auch noch vorgekaut wird, dann ist die Wahrscheinlichkeit, dass du den Beweis auch wirklich verstehst zumindest gegeben.

 

[Brombeere]

Dein Induktionsbeweis ist mir schon klar und ich weiß auch, dass man es so beweisen kann. Für diese Aufgabe ist aber gefordert, dass man streng nach diesem Schema vorgeht:
1. u0 > 0
2. u_i+1 < u_i - d für alle i und einen festen Wert d > 0
3. Für ui ≤ 0 wird die Schleife nach der i-ten Iteration verlassen

Also: 1.Bedingung beweisen, 2. Bedingung und 3. Bedingung. Mir erscheinen meine Beweise zu 1 und 2 korrekt zu sein. Allerdings habe ich Probleme die 3. Bedingung zu beweisen, und da suche ich eben Hilfe.

 

[Brombeere]

Ach, entschuldigung. Ich hab deinen Beitrag nicht genau gelesen...