Terminierung von imperativen Algorithmen

[chillerStudent]

Guten Tag,

folgender Programmabschnitt liegt vor mir:

double[] a = new double[10];
for (int k = 0; k < a.length; ++k) {
a[k] = Math.random();
}
double d = 10.0;
int i = 0;
while (i < d) {
if (a[i % 10] < 0.5) {
d += a[i % 10];
}
i++;
}

Und ich muss anhand folgender 5 Punkte nachweisen, dass die while schleife terminiert:

Konstruieren Folge von Werten u_0 u_1 u_2 u_3 ... wie folgt:
1. Bei Eintritt in die Schleife hat u_0 einen positiven Wert
2. Der Schleifenrumpf berechnet u_{i+1} aus ui
3. Es gilt u_{i+1} < u_i für alle i
4. Alle ui sind größer 0. Für ui+1≤ 0 wird die Schleife verlassen
5. Für alle i gilt: u_i – u_{i+1} > gamma > 0, für festen Wert gamma. (muss für
ganzzahlige ui nicht nachgewiesen werden)

Mein Ansatz:
1. mein u_0 ist die variable i und i=0.
2. offentsichtlich, wegen i++

Kann das bis hier hin stimmen? Bitte um Hilfe, Danke euch schon mal im Vorraus.

 

[muckelzwerg]

In welchem Zusammenhang machst Du das?
Eigentlich gibt es für sowas "Rechenregeln" für partielle und totale Korrektheit.
(Totale Korrektheit von While-Schleifen
Korrektheit und Terminierung)
Diese Formeln stecken in Deinen Bedingungen drin und entsprechen im Wesentlichen einer Induktion.
Ich vermute mal, dass ihr das jetzt "von Hand" zusammenbasteln und euch damit erstmal anfreunden sollt?

Dann frag Dich mal, warum Du bei Punkt 3 aufgehört hast.

 

[chillerStudent]

Erstmal Danke für deine Antwort.
Du hast Recht, wir behandeln gerade das Thema Korrektheit. Aber ich verstehe dieses Thema nicht so ganz.

Bei Punkt 3 hab ich aufgehört, weil ich nicht weiß wie ich das Beweisen soll, also dass u_i+1 < u_0 ist.

 

[muckelzwerg]

Du kannst es nicht beweisen. Wenn Du u als i wählst, dann wird i immer größer. Also gilt u_{i+1} > u_i.
Dann musst Du Dir was anderes überlegen. Schau Dir mal die Abbruchbedingung in Punkt 4 an.
Was musst Du für u wählen, damit irgendwann u_{i+1} <= 0 gilt?

Und überleg Dir vorher mal ob diese Schleife wirklich garantiert abbricht und wann und warum sie das tut. Das sollte Dir bei der Suche nach der Invarianten helfen.

 

[F.S.WhiTeY]

manchmal hilft es auch, sich das ganze vor augen zu halten.

Implementier den code doch mal und lass dir bei jedem schleifendurchlauf eine tabelle/aufstellung der werte geben und schau dir an ob und wann die whileschleife abbricht.

dann siehst du zumindest schon mal was passiert. der rest muss so wie muckelzwerk gesagt hat rechnerisch geschehen.

 

[chillerStudent]

Also, folgende Daten habe ich erhalten....hab es so wie erwünscht in einer Tabelle ausgeben lassen und dabei festgestellt, dass die Schleife erst dann abbricht, wenn i größer als d wird...aber dabei verstehe ich immernoch nicht ( schade aber wahr ) welchen Variable u annehmen muss damit man zeigen kann dass u<0 wird....

Meiner Ansicht nach denke ich, dass d < i -> dem entspricht U(i+1) <= Ui ???

 

[chillerStudent]

Also hab einen zweiten Anlauf genommen...hier habe ich mich bisschen mehr angestrend und festgestellt....ich trag einfach die antworten nacheinander...

1. Wegen U0 = d und wegen while bedingung ist U0>0
2. offentsichtlich nach Konstruktor
3. a[..] ist Ui+1 und d ist Ui...also entspricht nach jedem Durchlauf Ui+1 <= Ui
Bsp... a[..]=0.2936... -> Ui+1
d=10.0 -> Ui
Ui+1<Ui
4. Wegen Schleifenbedingung und d=10.... ist Ui>0
Wenn Ui+1<=0, dann folgt, d hat maximalwert und somit ist die Schleifenbedingung erfüllt.
5. Man kann einen beliebigen Wert für i aus der For-Schleife nehmen....daraus folgt
Ui - Ui+1 > 0, z.B.: 10.0 - 0.29396... ist größer 0

?????? Ich bin mir ehrlich gesagt garnicht sicher, es ist nur so ein gedankenblitz..

 

[muckelzwerg]

Als mal langsam. Dass die Schleife abbricht, wenn i größer als d ist, das sollte Dir eigentlich schon klar gewesen sein.

Für die Invariante u brauchst Du einen Term und nicht bloß einen einfachen Wert.
Wenn i in jedem Schritt größer wird, dann muss es doch eher etwas in der Form "u = ? - i" mit ? > 0 sein, damit u kleiner werden
und unter Null fallen kann.
Welcher Wert bietet sich da denn an? Denk besonders mal an die Abbruchbedingung.
Wenn in der Schleife (i < d) nicht mehr erfüllt ist, wird abgebrochen. Im gleichen Durchlauf muss also "u <= 0" erfüllt sein.

 

[chillerStudent]

Meinst du
u=d-i mit d>0 ??

 

[muckelzwerg]

Kannst Du das nicht selbst herausfinden? Wenn Du es nicht prüfen kannst, dann erzähl ich Dir hier irgendwas und Du übernimmst das?
Ich hab das jetzt auch schon eine Weile nicht mehr gemacht. Vielleicht irre ich mich ja auch. Wer weiß ...
Also versuch es mal mit u = d - i und prüfe die Bedingungen durch.

 

[chillerStudent]

Meinst du
u=d-i mit d>0 ??

Ich meine, dass das richtig ist, weil am ende ja i größer d wird und damit u<0.

Könntest du vielleicht bitte was zu meinem Beitrag von 18:41 Uhr sagen?

 

[muckelzwerg]

Ja. Der ist total wirr, hat keine klare Aussage welchen Wert Du für u gesetzt hast und alle Bedingungen werden durcheinander zurechtgeredet.
Und FALLS das u = d sein soll, ist er ganz offensichtlich falsch, denn d wird niemals <= 0. Schon gar nicht im Moment des Abbruchs.

Ist nicht bös gemeint, aber wenn ich die Hausaufgabe SO von Dir bekäme würde ich Dir nicht gerade allzuviele Punkte dafür geben.
Schreib doch ausführlich und verständlich die Herleitungen hin. Du kannst sie ja für den Unterricht ausdrucken, wenn Du sie nicht nochmal abschreiben willst. Dann siehst Du auch wo es überall nicht passt.

 

[chillerStudent]

Oh man ich versteh nichts mehr. u wird ja nie negativ. ich rechne hier ganze zeit immer größer minus kleiner

 

[muckelzwerg]

Verwende u = d - i
Gehe damit eine Bedingung nach der anderen durch und leite ab, ob sie erfüllt ist. Höre nicht auf, wenn Du eine der Bedingungen nicht ableiten kannst, sondern mach mit der nächsten weiter.
Schreibe alles ausführlich auf und zeige es hier. DANN schau ich mir das auch nochmal an.

Die Chancen, dass Dir das jemand schenkt, sind ziemlich gering. Es ist ja fast nur formale Schreibarbeit.
Frag Dich mal, was uns unsere eigene Zeit wert ist und wie "positiv" Deine Auseinandersetzung mit der Aufgabe aussieht.
Ich will nicht zu sehr auf die Kacke hauen, aber anstatt hier Zeit aufzuwenden und Dir den Kram zu erklären (oder gar die Lösung hinzuschreiben) kann ich auch arbeiten gehen, mit meinen Freunden feiern oder vor dem Fernseher gammeln.
Ich werde mich ganz sicher nicht umfangreicher um DEINE Aufgabe kümmern, als DU es selbst tust.