Seite 1 von 1

Übung 8 Aufgabe 2

Verfasst: 10. Mär 2011 19:48
von patrix
Hallo zusammen,
ich habe mit dem Lösen von Übung 8 Aufgabe 2 eigenlicht keine Probleme. Ich wollte jetzt jedoch eine operation wie x:=0; if x<=0 then x:=5 else x:=4 fi; herleiten scheitere aber schon im Ansatz.

Kann mir jemand auf die Sprünge helfen - besonderst bei der Aufteilung der beiden Behfehle c1 = x:=0; und c2 if x<=0 then x:=5 else x:= 4 fi; ?

P.S. mit den Kalkülen aus der Musterlösung???

Danke und Grüße

Patrick

Re: Übung 8 Aufgabe 2

Verfasst: 10. Mär 2011 21:53
von JanM
Ich muss gleich sagen ich verstehe den Sinn von dem Kalkül aus der Musterlösung nicht wirklich, aber ich wäre so vorgegangen:
von deinem programm kommt man in einem primitiven Berechnungsschritt zu "<if x<=0 then x:=5 else x:=4,\sigma[x\0]>" diesen schritt kann man mit den kalkülregeln herleiten.
nun nimmt man dieses programm und macht wieder einen Berchnungsschritt zu "<x:=5,\sigma[x\0]>", welcher sich ebenfalls mit dem Kalkül herleiten lässt. Diesen kann man dann zu "<\epsilon,\sigma[x\5]>" berechnen (auch im Kalkül herleitbar) und somit erhält man die terminierung des programms.
Ich habe also jeden primitiven Berechnungsschritt, der intuitiv klar ist, gezeigt, dass er ebenfalls im Kalkül herleitbar ist.
Aber im gegensatz zu den anderen kalkülen habe ich halt mehrere einzelne Herleitungen gebraucht.

Re: Übung 8 Aufgabe 2

Verfasst: 10. Mär 2011 22:18
von hymGo
Ich würde sagen man verwendet dieses Kalkül zusammen mit dem Urteil aus Modul 8 Folie 14. Dann bekommt man die "einzelnen Teile" zusammen.

Re: Übung 8 Aufgabe 2

Verfasst: 11. Mär 2011 08:49
von patrix
Hallo zusammen,
ich glaube das die Anwendung einzelner Kalkülregeln hier besser ist, denn die Angesprochenen Urteile sind ja berechnungen von Aritmetischen Ausdrücken.

Jedenfalls aber vielen Dank und viele Grüße

Patrick

Re: Übung 8 Aufgabe 2

Verfasst: 11. Mär 2011 15:01
von FRED0815
Hi

Ich hab mir da mal Gedanken gemacht und ich denke:

Das mit der Alternativen Semantik für Bexp also dem Urteil \(\langle b,\sigma \rangle \rightarrow_1 b'\) (wie beschrieben) man nur Urteile herleiten kann die in einem primitiven Berechnungsschritt herleitbar sind.
Also z.B. ist:
\(\langle \neg (3=2), \sigma \rangle \rightarrow_1 true\)
nicht in einem primitiven Berechnungsschritt herleitbar (siehe: http://www.fachschaft.informatik.tu-dar ... 96&t=21184). Damit die Forderung der Angemessenheit erfüllt ist: Also informell: Alles was ich mit Bexp herleiten kann muss ich auch mit der Alternativen Semantik für Bexp herleiten können; müssen das Urteil \(\langle b,\sigma \rangle \Rightarrow t\) definiert werden (wir für die Alternative Semantik für Com oder Aexp).

Im prinzip das was vorher(oben) schon gesagt wurde nur präzisiert.


mfg Fred