---

Geschrieben von JanS am 17.01.2009 um 01:48:

  Hoare Kalkül

Hallo
Folgende Aufgabe mit der ich nicht zurecht komme..:

{true}

x=5
res=x*x-6
re=res mod 5

{res=4}

ich kann mit der Vorbedingung nix anfangen bzw weiß nich wie ich die einsetzen soll..

mfg
Jan

---

Geschrieben von kiste am 17.01.2009 um 13:27:

 

Das heißt einfach das es keine Vorbedingung gibt.
Fange einfach an:
{true}
x = 5
{true ^ x=5} = {x=5}
etc.

---

Geschrieben von JanS am 17.01.2009 um 14:54:

 

wir haben das im Tutorium so aufgeschrieben:

{Nachbed.[Zuweisung]}Anweisung{Nachbed.}
-----------------------------------------------
{Vorbed.}Anweisung{Nachbed.}

Aber das bekomm ich bei der Aufgabe ja nicht in diese Form
bzw hae ich dann drei mal das selbe dastehn..
Und wie schreibe ich die Variable auf die ja erst in einer Zuweisung entsteht?

---

Geschrieben von kiste am 17.01.2009 um 15:10:

 

Es ist ja egal welchen Wert x davor hatte. Du kannst auch x=a für ein bestimmtes a bzw. x=undef. annehmen.

---

Geschrieben von JanS am 18.01.2009 um 11:50:

 

1.
{true[x<--5]}x=5{x=5}
---------------------------------
{x=5}x=5{true}

Ist eine notation sinnvoll in der 4 mal das selbe steht? :P

Was ist denn jetzt die nächste nachbedingung??
Abgesehn davon das man auch die Konsequenzregel anwenden könnte.. aber wir solln das mit zwischenschritten machen..

komm da echt nicht weiter.. obwohl es so kompliziert nicht aussieht...

mfg
Jan

---

Geschrieben von JanS am 18.01.2009 um 14:15:

 

1
{true[x<--5]}x=5{x=5}
---------------------------------
{x=5}x=5{true}


2
{x=5[res<--x*x-6]}res=x*x-6{res=19}
------------------------------------------------------
{res=5*5-6}res=x*x-6{res=19


3
{res=4[res<--res mod 5]}res=res mod 5{res=4}
-------------------------------------------------------------------
{res mod 5=4}res mod 5{res =4}



ist das der sinn und zweck des hoare kalküls?

---

Geschrieben von JanS am 18.01.2009 um 16:06:

 

Hm
Kann mir dss evtl nochmal wer erklären.. ich hab schon alles im internet über hoare gelesen.. aber ich verstehs nich...