Diskussion:Schleifeninvariante

Widersprüchlich

Erst heißt es, eine einfaches true sei bereits eine Schleifeninvariante, und ein wenig später heißt es dann, es gäbe keinen Algorithmus um eine Schleifeninvariante zu bestimmen.. (nicht signierter Beitrag von 46.115.100.87 (Diskussion) 14:54, 9. Jun. 2013 (CEST))

Das ist richtig, eine Tautologie stellt immer eine Schleifeninvariante dar. Allerdings ist diese nicht notwendigerweise hilfreich um die Korrektheit der Schleife zu beweisen (was mit der zweiten Aussage "Es gibt keinen Algorithmus um eine Schleifenvariante zu bestimmen" gemeint ist).

Um die Korrektheit einer Schleife zu beweisen, muss ein formales Ziel der Schleife definiert sein. Dieses Ziel muss sich durch Und-Verknüpfung aus der Invariante und der abweisenden Schleifenbedingung (beides gilt nach der Schleife) ergeben (siehe Hoare-Kalkül). Wenn du dir das Beispiel anschaust, dann ist das formale Ziel der Schleife p = x * y, die Multiplikation aus x und y. Die abweisende Schleifenbedingung ist x = 0, wenn sie eintritt bricht die Schleife ab. Nun ist es nicht möglich aus einer Tautologie (true) und x = 0 das formale Ergebnis p = x * y abzuleiten. Daher muss eine ausgereiftere Invariante, z.B. (x * y) + p = a * b gewählt werden. Wird diese mit der abweisenden Schleifenbedingung x = 0 verknüpft. Das ergibt (0 * y) + p = a * b was p = a * b ist. Damit ist die formale Korrektheit der Schleife bewiesen.

Ich habe einige Anpassungen vorgenommen. Ich hoffe es kommt jetzt klarer rüber. --Tfr.didi (Diskussion) 03:42, 5. Apr. 2014 (CEST)

Beweis

Es ist bewiesen, dass es keinen Algorithmus gibt, der eine Schleifeninvariante automatisch bestimmt.

Für diese Aussage sollte eine Quelle angegeben werden. --Selby (Diskussion) 00:10, 3. Apr. 2014 (CEST)

Schleife im Beispiel ist nicht korrekt

multiply(-1, b) = 0 ≠ (-1 • b). Für die Schleife ist die Invariante ((x • y) + p = (a • b)) ∧ (x ≥ 0). (nicht signierter Beitrag von 194.138.39.59 (Diskussion) 14:19, 23. Okt. 2014 (CEST))