Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Klausur 21.2.2008 A10 d,e
Bei mir is grad die Weltanschauung gekippt!
Eine Schleifeninvariante kann auch Invariante der Schleife sein, wenn sie vor betreten der Schleife nicht gilt?
Hier: (y-y0)/(x-x0)=m hätt ich prinzipiell ausgeschlossen, weil bei den Variablenzuweisungen 0 im Nenner steht?
Für den Beweis bei e) brauch ich aber genau die!
an der Aufgabe hab ich mir auch schon den Kopf zerbrochen.
Aber (y-yo)/(x-x0) = m gilt vor der Schleife, weil da ja auch gelten muss y1=y0 und x1=x0. Aber wie machst du den Beweis dass Sie in der Schleife gilt??
Da komme ich nur auf:
(y+m-y0)/(x+1-x0) = m und kann darin irgendwie nicht zeigen dass sie gilt…
Eine Bedingung I ist Invariante der Schleife
while (b) { A }wenn gilt: b && I => wp(A, I).
Falls I falsch ist, steht da “falsch => wp(A, I)”
Nach den Logik-Rechenregeln ist diese Aussage wahr.
Damit ist die Bedingung “false” Schleifeninvariante, genauso wie “true”.
Bei der vorliegenden Klausuraufgabe ist es nun so, dass I zu Beginn der
Schleife nicht gilt, aber nach mindestens einem Schleifendurchlauf ANFÄNGT zu gelten.
Damit kann man die Schleifeninvariante nutzen, indem man gleichzeitig argumentiert
dass die Schleife tatsächlich mindestens einmal durchlaufen wird.
Im Allgemeinen sind Schleifeninvarianten die nicht gelten nutzlos, da man aus ihnen keine Nachbedingungen herleiten kann.
Allerdings fangen sie an nützlich zu werden, wenn man z.B. beweisen kann dass sie irgendwann anfangen gültig zu werden.
Ja eine Schleifeninvariante ist etwas das in der Schleife invariant ist, also sich nicht veraendert und [m]false[/m] veraendert sich nicht.
Kann mir bitte trotzdem noch jemand erklären wie ich in dieser Klausuraufgabe damit zeige dass die Invariante in der schleife gilt?
Bei Mir folgt aus b&&I => (y+m-y0)/(x+1-x0)=m. Und das macht doch keinen Sinn?
Falsch.
Der Wert einer Schleifeninvariante darf sich von False auf True ändern.
Er darf sich NICHT von True auf False ändern…
Anders formuliert: Eine Bedingung ist Schleifeninvariante, wenn sie sich durch die Schleifenbodyausführung NICHT von True auf False ändert.
Du argumentierst, dass die Invariante nach der ersten Schleifendurchführung gilt.
Dann ist x=x0+1 und y = y0+m, und damit (y-y0) / (x-x0) == m/1 == m.
Dann beweist du genau so wie sonst, dass die Bedingung invariante ist.
Ok, aber im Schleifenrumpf steht ja x=x+1 und y=y+m. Wieso darf man das hier einfach in x=x0+1 und y = y0+m umwandeln?
Weil x vor der Schleife auf x0 initialisiert wird, denke ich.
Wenn ich mich richtig an die Aufgabe erinnere muss man aber keine derart ausführliche begründung abliefern…
Stimmt. Oh, Logik ich wuerde dir gerne in den … treten.
D.h. [m]I = i>0[/m] ist gueltige Schleifeninvariante der Schleife:
for(int i=-13; i<42; i++){ }weil ja [m]b & I → wp(A,I)[/m] gilt.
… dann sollte ich wohl aufhoeren Schleifeninvariante mit invariant zu erklaeren, da es zumindest im logischen Sinne falsch ist.