Übung 8 Aufgabe 2

patrix
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 16. Nov 2009 17:10

Übung 8 Aufgabe 2

Beitrag 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

Benutzeravatar
JanM
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 157
Registriert: 24. Aug 2010 10:58

Re: Übung 8 Aufgabe 2

Beitrag 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.

Benutzeravatar
hymGo
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 209
Registriert: 4. Okt 2009 23:17

Re: Übung 8 Aufgabe 2

Beitrag 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.

patrix
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 16. Nov 2009 17:10

Re: Übung 8 Aufgabe 2

Beitrag 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

FRED0815
Neuling
Neuling
Beiträge: 5
Registriert: 20. Dez 2010 18:23

Re: Übung 8 Aufgabe 2

Beitrag 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

Antworten

Zurück zu „Archiv“