Beweis durch Hoare Kalkül

[blackwidow83]

Hallo Ihr Lieben,

ich muss ein Stück einfachen Programmcode durch das Hoare Kalkül beweisen und komm mit der ganzen Thematik absolut nicht klar. Auch nach dem Belesen auf mehreren Webseiten und diversen Vorlesungen, gehts irgendwie nicht weiter und ich brauch mal Eure Hilfe.

Folgender Code soll mit Hoare auf Korrektheit überprüft werden:

{k*j+k*i+k > 80}

i := i + 1;

j := j + i;

k := k * i;

{k > 80}

Wie geht man an soetwas heran?

Gruß

[beebof]

Wie geht man an soetwas heran?

Ich hab sowas immer "rückwärts" gemacht. Also: die Endaussage nehmen, die Variablen darin durch das vorhergehende ersetzen usw.

btw. in der letzten Zeile meinst du sicher

k:=k*j;

oder?

Soll ich mal vormachen?

{k*j+k*i+k > 80}

i := i + 1;

j := j + i;

{k*j > 80}

k := k * j;

{k > 80}

Ich denke, den Rest kriegst du so alleine hin. Ist eigentlich ganz einfach.

[blackwidow83]

Hey beebof,

besten Dank. Dass man das rückwärts am einfachsten macht, habe ich auch schon gelesen/gehört. Dieses Einsetzen wollte ich auch machen, aber ist das wirklich die Beweisführung? Wir haben in der Vorlesung so komplizierte Beweisbäume kennengelernt, die von unten nach oben wachsen und in denen ich diverse Beweisregeln so lange ausführen kann, bis die einzelnen Äste des Baumes "true" werden. Sind das nur evrschiedene Wege der Beweisführung?

Gruß

Basti

[beebof]

... aber ist das wirklich die Beweisführung?

Ich habs zumindest so gelernt (Informatik I). Und meiner Meinung nach ist das auch legitim, da man nur Äquivalenzumformungen durchführt.

[Klotzkopp]

Und meiner Meinung nach ist das auch legitim, da man nur Äquivalenzumformungen durchführt.

Ich bin mir da nicht so sicher. Bei Ungleichungen dreht sich das Zeichen um, wenn man mit negativen Zahlen multipliziert. Eine Unterscheidung nach dem Vorzeichen von j könnte also notwendig sein.

[beebof]

Eine Unterscheidung nach dem Vorzeichen von j könnte also notwendig sein.

Ich denke nicht, da ich mit der Bedingung k:=k*j umforme. (bzw. im "rückwärtigen" Fall k*j := k)

Ich substituiere also einfach nur die Aussage k > 80. Hierbei brauche ich nicht auf Vorzeichen achten, da sich diese nicht ändern dürfen.