Hoare Kalkül

Neue Frage »

Auf diesen Beitrag antworten »
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
 
Auf diesen Beitrag antworten »
kiste

Das heißt einfach das es keine Vorbedingung gibt.
Fange einfach an:
{true}
x = 5
{true ^ x=5} = {x=5}
etc.
Auf diesen Beitrag antworten »
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?
Auf diesen Beitrag antworten »
kiste

Es ist ja egal welchen Wert x davor hatte. Du kannst auch x=a für ein bestimmtes a bzw. x=undef. annehmen.
 
Auf diesen Beitrag antworten »
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
Auf diesen Beitrag antworten »
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?
Auf diesen Beitrag antworten »
JanS

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


Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »