Hoare - Invariante finden < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Aufgabe | {true}
r = -1;
i = 0;
while ((i [mm] \le [/mm] n) [mm] \wedge [/mm] (r == -1)) {
if (i*i == n)
r = i;
else
i = i + 1;
}
{(i =sqrt(n)) [mm] \vee [/mm] (r < 0)} |
Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt.
Ich soll für dieses Programm passende Asserts eintragen. Dazu muss ich zu Beginn eine gute Schleifeninvariante finden.
Leider finden ich hier keinen passenden Ansatz.
|
|
| |
|
Bei dieser einfachen Schleife gibt es keinen Sinn, eine Schleifeninvariante zu bilden. Es geht ja normalerweise darum, zu zeigen, dass die Schleife irgendwann beendet wird. Da beim Durchlaufen i immer um 1 erhöht wird, ist i irgendwann (bei negativem n schon zu Anfang) [mm] \ge [/mm] n, und die Schleife wird verlassen.
Wenn du unbedingt eine Invariante brauchst, kannst du n selber nehmen oder, falls das irgendwie dynamischer aussehen soll, n-i+i, was aber ebenso wenig bringt.
Ich kenne deine Programmiersprache nicht (vermutlich c?) und nehme an, dass die letzte Zeile eine logische Ausgabe der Berechnung sein soll. Falls das der Fall ist: Ist dir klar, was das Programm überhaupt für eine Funktion hat? Falls nicht, kann ich eine Vermutung äußern.
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 08:43 Mi 08.06.2016 | | Autor: | Willi1106 |
Hallo,
danke für die Anwort.
Das Program sollte in C sein.
Die Ausdrücke zu Beginn und am Ende sind Asserts und sollten somit immer Wahr sein.
Das Program soll i solange erhöhen, bis i die Wurzel von n ist. Falls dies nicht geschieht, bricht das Programm bei n ab.
Die Schleifeninvariante sollte auch ein Boolscher Ausdruck sein.
Ich denke Richtung (0 [mm] \le [/mm] i [mm] \le [/mm] n+1) [mm] \wedge [/mm] (r [mm] \le [/mm] i).
Aber bin nicht sicher, ob diese Sinnvoll ist.
|
|
|
| |
|
Das ursprüngliche Programm bricht immer irgendwann ab, und zwar entweder dann, wenn i*i=n ist, also wenn n eine Quadratzahl ist, oder, falls nicht, wenn i=n+1 ist. In beiden Fällen gibt dir das Programm aber den Wert TRUE zurück, und du erfährst gar nicht, was nun wirklich los war - sollte man meinen!
Betrachten wir die Sache genauer.
Ist n z.B. 24, bleibt r auf -1 und i läuft bis 25 durch. Am Ende ist r=-1, und wegen der oder-Verknüpfung erhältst du TRUE.
Ist n z.B. 25, so wird bei i=5 r auf 5 gesetzt. Nach Verlassen der Schleife ist nun [mm] r\ne [/mm] -1, aber i=sqrt(n), und deshalb kommt wieder TRUE heraus - sollte man meinen!
Tatsächlich passiert aber im letzten Schritt folgendes:
i ist 5. sqrt(25) ist auch fünf - sollte man meinen! Tatsächlich führt der Rechner eine Real-Operation aus, und obwohl sqrt(25)=5 sein müsste, kann der Rechner aufgrund seines Algorithmus wegen Rundungsfehlern auf 4,9999999999 oder 5,0000001. kommen. Und dann ist eben sqrt(25) nicht 5, und du erhältst die Antwort FALSE.
Das Programm prüft somit, ob sqrt - auf Quadratzahlen angewandt - wirklich die Wurzel zurückliefert oder evtl. einen ungenauen Wert. Das kann fatale Folgen haben, wenn du z.B. in einem Primzahlprogramm, in dem du mit sqrt arbeitest, 25 als Primzahl ausgedruckt bekommtst.
Und nun rate mal, woher ich das wohl weiß...
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig | | Datum: | 15:20 Do 09.06.2016 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
