Aufgabe 5.4a

mProg
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 147
Registriert: 25. Apr 2015 00:10

Aufgabe 5.4a

Beitrag von mProg »

Hallo ich habe eine Frage bzgl der Lösung dieser Aufgabe:
für r; sind die Prämisse <c1,zigma,pi>-><c1,zigma2,pi2> <c2,zigma2,pi2>-><c2,zigma1,pi1> gegeben.
Kann man nicht die Prämisse so schreiben:
<c1,zigma,pi>-><c1,zigma1,pi> <c2,zigma1,pi>-><c2,zigma1,pi1> gegeben.
Wenn nicht, warum?

Markus Tasch
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 124
Registriert: 11. Sep 2015 10:57

Re: Aufgabe 5.4a

Beitrag von Markus Tasch »

Die Regel muss wie in der Musterlösung

\(r; \frac{\langle c_1, \sigma, \pi \rangle \rightarrow \langle \sigma'',\pi''\rangle \quad \langle c_2, \sigma'', \pi'' \rangle \rightarrow \langle \sigma',\pi'\rangle}{\langle c_1;c_2, \sigma,\pi \rangle \rightarrow \langle \sigma',\pi'\rangle}\)

sein (beachte, dass die Kommandos nur zu einem neuen Zustandspaar asuwerten und nicht zu einem Kommando+Zustandspaar).

Dein (korrigierter) Vorschlag

\(r; \frac{\langle c_1, \sigma, \pi \rangle \rightarrow \langle \sigma',\pi'\rangle \quad \langle c_2, \sigma', \pi' \rangle \rightarrow \langle \sigma',\pi'\rangle}{\langle c_1;c_2, \sigma,\pi \rangle \rightarrow \langle \sigma',\pi'\rangle}\)

beachtet nicht die Möglichkeit, dass \(c_2\) den Zustand potentiell ändern könnte. Beispielweise könnte \(c_2\) eine Zuweisung sein und damit einer Variablen einen neuen Wert zuweisen. Demetnsprechend muss die Möglichkeit bestehen, das der Zustand nach der AUsführung von \(c_1\) nicht \(\langle \sigma',\pi'\rangle\) ist, sondern ein alternativer dritter Zustand.
Markus Tasch, M.Sc.
Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt
http://www.mais.informatik.tu-darmstadt.de

schnubbes
Neuling
Neuling
Beiträge: 7
Registriert: 16. Okt 2013 18:08

Re: Aufgabe 5.4a

Beitrag von schnubbes »

Hierzu habe ich auch noch zwei Fragen.
Die Aufgabe ist "Definieren Sie Kalkülregeln zur Herleitung von Instanzen der Urteile [...] \(\langle \texttt{while b do c od}, \sigma, \pi \rangle \rightarrow \langle \sigma' \pi' \rangle\)".

Hier habe ich nur die Kalkülregel zu \(\texttt{rwht}\) definiert, da \(\texttt{rwhf}\) in dem Zustandspaar \(\langle \sigma, \pi \rangle\) bleibt und, nicht wie in der Aufgabenstellung gefordert (?), zu \(\langle \sigma', \pi' \rangle\) übergeht. Wie ist die Aufgabenstellung hier zu verstehen?

Und warum werden die arithmetischen bzw. booleschen Ausdrücke bei den entsprechenden Regeln nur im Zustand \(\sigma\) ausgewertet? Ist es falsch die Ausdrücke im Zustandspaar \(\sigma, \pi\) auszuwerten? Zum Beispiel für \(r :=\):

\(r := \frac{\langle a, \sigma, \pi \rangle \Downarrow n}{\langle X := a, \sigma, \pi \rangle \rightarrow \langle \sigma', \pi \rangle} \sigma' = \sigma[X\backslash n]\)

Gruß.

Markus Tasch
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 124
Registriert: 11. Sep 2015 10:57

Re: Aufgabe 5.4a

Beitrag von Markus Tasch »

Die Aufgabe ist "Definieren Sie Kalkülregeln zur Herleitung von Instanzen der Urteile [...] \(\langle whilie \; b \; do \; c \; od,\sigma,\pi\rangle \rightarrow \langle \sigma',\pi'\rangle\)".

Hier habe ich nur die Kalkülregel zu rwht definiert, da rwhf in dem Zustandspaar \(\langle\sigma,\pi\rangle\) bleibt und, nicht wie in der Aufgabenstellung gefordert (?), zu \(\langle\sigma',\pi'\rangle\) übergeht. Wie ist die Aufgabenstellung hier zu verstehen?
Die Regel rwhf muss hier auch definiert werden. Bei \(\sigma',\pi'\) handelt es sich ja nur um Variablen. Damit ist also nicht gegeben, dass diese nicht mit \(\sigma,\pi\) in der Definition der Regel instanziert werden oder in der Seitenbedingung \(\sigma'=\sigma \land \pi'=\pi\) gefordert. Beides würde dir erlauben, die neue Regel für rwhf zu definieren. Dementsprechend fordert die Aufgabenstellung auch nicht, dass \(\neg \sigma'=\sigma\) bzw. \(\neg \pi'=\pi\) gelten, wie von dir implizit angenommen.

Und warum werden die arithmetischen bzw. booleschen Ausdrücke bei den entsprechenden Regeln nur im Zustand \(\sigma\) ausgewertet? Ist es falsch die Ausdrücke im Zustandspaar \(\sigma,\pi\) auszuwerten?
Die kurze Antwort ist: Ja das ist falsch.

Erklärung:
Das Urteil \(\langle a,\sigma,\pi \rangle \Downarrow n\) (bzw. \(\langle b,\sigma,\pi \rangle \Downarrow t\) für boolesche Ausdrücke) ist nicht definiert. Dementsprechend kann man das auch nicht verwenden ohne es zu definieren und dann auch das komplette entsprechende Kalkül zu definieren.
Wenn du \(\langle a,\sigma,\pi \rangle \Downarrow n\) bzw. \(\langle b,\sigma,\pi \rangle \Downarrow t\) nutzen möchtest, müsstest du die Urteile erst einführen und entsprechende Kalküle definieren. Die Kalküle wären diesen Fall natürlich einfach analog zu den Kalkülen für \(\langle a,\sigma \rangle \Downarrow n\) bzw. \(\langle b,\sigma \rangle \Downarrow t\).

In dieser Aufgabe ist das aber einfach nicht notwendig, da die arithmetischen und booleschen Ausdrücke nicht mit dne neu eingeführten Listen arbeiten. Dementsprechend reicht das alte Kalkül um deren Semantik zu definieren.
Markus Tasch, M.Sc.
Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt
http://www.mais.informatik.tu-darmstadt.de

Antworten

Zurück zu „Archiv“