Übung 9 Aufgabe 1 Hoare Logik

dees
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 6. Mär 2011 14:01

Übung 9 Aufgabe 1 Hoare Logik

Beitrag von dees »

Hallo,

mir ist die Programm-Spezifikation mit Hoare-Logik nicht so ganz klar.

1) Wie wähle ich die Vorbedinung? In der Übung 9.1 wird "x>=0" gewählt aber warum ist das so? Wenn es darum geht überhaupt die Schleife auszuführen müsste es doch "x>=1" sein da wir bei den natürlichen Zahlen ja nicht kleiner als 0 werden (wegen z <= x-1)?

2) Warum kann ich als Vorbedingung nicht gleich die Schleifenbedingung "z<=x-1" wählen?

3) Warum lautet die Schleifeninvariante jetzt I(x,y,z) := y = z*z ^ z <= x und nicht I(x,y,z) := y = z*z ^ 0 <= x ?

greetings

danny
Mausschubser
Mausschubser
Beiträge: 51
Registriert: 17. Okt 2010 22:32

Re: Übung 9 Aufgabe 1 Hoare Logik

Beitrag von danny »

zu 1):
Ein Hoare-Tripel besagt ja, dass wenn die Vorbedingung gilt und das Programm ausgeführt wird, danach die Nachbedingung wahr ist. Egal ob oder wie oft die Schleife innerhalb des Programms ausgeführt wurde.
Ich habe zuerst die Nachbedingung aufgestellt, also y = x^2
Dann muss man sich überlegen, welche Vorbedingungen gelten müssen, damit die Nachbedingung auf jeden Fall wahr wird. Für Zahlen x >= 0 berechnet das angegebene Programm tatsächlich die Quadratzahl von x, für x kleiner 0 jedoch nicht. Deswegen kommt man auf die Vorbedingung, dass x >= 0 gelten muss.

zu 2):
Diese Vorbedingung ist nicht sinnvoll, denn es ist ja durchaus ok das Programm mit x = 5, y = 10, z = 12 aufzurufen, denn y und z werden direkt am Anfang sowieso auf 0 gesetzt. Deine Vorbedingung würde diesen Aufruf allerdings ausschließen.

dees
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 6. Mär 2011 14:01

Re: Übung 9 Aufgabe 1 Hoare Logik

Beitrag von dees »

Das macht soweit Sinn, danke.

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Übung 9 Aufgabe 1 Hoare Logik

Beitrag von fscheepy »

danny hat geschrieben: Für Zahlen x >= 0 berechnet das angegebene Programm tatsächlich die Quadratzahl von x, für x kleiner 0 jedoch nicht. Deswegen kommt man auf die Vorbedingung, dass x >= 0 gelten muss.
Wie sieht es denn für x = 0 aus? Gilt dann etwa z <= x-1? Inwiefern wird die Tatsache behandelt, dass es sich hier (soweit ich das verstanden habe) um natürliche Zahlen handelt? Gilt dann 0 - 1 = 0? Wenn es aber natürliche Zahlen sind, warum muss man dann überhaupt schreiben, dass x >= 0 ist?
dees hat geschrieben: 3) Warum lautet die Schleifeninvariante jetzt I(x,y,z) := y = z*z ^ z <= x und nicht I(x,y,z) := y = z*z ^ 0 <= x ?
Ich verstehe nicht so recht, wie man überhaupt systematisch auf diese Invariante kommt. Kann das jemand vielleicht erklären?

/edit: Warum muss man eigentlich über die Nachbedingung Q von z nichts aussagen?

danny
Mausschubser
Mausschubser
Beiträge: 51
Registriert: 17. Okt 2010 22:32

Re: Übung 9 Aufgabe 1 Hoare Logik

Beitrag von danny »

fscheepy hat geschrieben:Wie sieht es denn für x = 0 aus? Gilt dann etwa z <= x-1? Inwiefern wird die Tatsache behandelt, dass es sich hier (soweit ich das verstanden habe) um natürliche Zahlen handelt? Gilt dann 0 - 1 = 0? Wenn es aber natürliche Zahlen sind, warum muss man dann überhaupt schreiben, dass x >= 0 ist?
Die Vor- und Nachbedingung sagt ja: "Ist x >= 0 (Vorbedingung), so berechnet das Programm die Quadratzahl von x (Nachbedingung)". Das gilt auch für den konkreten Fall x = 0. Da z am Anfang des Programms auf 0 gesetzt wird, gilt z <= x - 1 natürlich nicht (wie in der Vorlesung definiert werden ganze Zahlen verwendet), also wird die Schleife kein mal ausgeführt. Trotzdem berechnet das Programm die Quadratzahl von x, denn in y steht ja das richtige Ergebnis, nämlich 0.

fscheepy
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 153
Registriert: 14. Dez 2009 21:17

Re: Übung 9 Aufgabe 1 Hoare Logik

Beitrag von fscheepy »

danny hat geschrieben:wie in der Vorlesung definiert werden ganze Zahlen verwendet
Du hast natürlich Recht, ich hab mich da von dem "N" verwirren lassen, aber in der Vorlesung wurde ja N als die 0, zusammen mit den positiven und negativen ganzen Zahlen definiert. Danke für den Hinweis. :)

Antworten

Zurück zu „Archiv“