| Die letzten 7 Beiträge |
| JanS |
Hm
Kann mir dss evtl nochmal wer erklären.. ich hab schon alles im internet über hoare gelesen.. aber ich verstehs nich... |
| JanS |
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? |
| JanS |
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 |
| kiste |
Es ist ja egal welchen Wert x davor hatte. Du kannst auch x=a für ein bestimmtes a bzw. x=undef. annehmen. |
| JanS |
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? |
| kiste |
Das heißt einfach das es keine Vorbedingung gibt.
Fange einfach an:
{true}
x = 5
{true ^ x=5} = {x=5}
etc. |
| JanS |
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 |
