Programmäquivalenz

lukas scheidel
Neuling
Neuling
Beiträge: 3
Registriert: 7. Mär 2017 09:11

Programmäquivalenz

Beitrag von lukas scheidel » 7. Mär 2017 09:19

Sei die Aufgabe x:=1 ~ x:=0;x:=x+1 und o steht für sigma und E für groß Sigma

Seien o,o' Zustände aus E für x:=1, also: < x:=1,o> -> o' , dann gibt es einen Zustand o* mit <x:=0;x:=x+1, o> -> o*
Ich möchte dann zeigen, dass gilt o' = o*, was ja offensichtlich ist.

Ich erhalte mit den Herleitungen: o' = o[x\1] für x:=1 und o''= o[x\0] und o* = o''[x\x+1] für <x:=0;x:=x+1, o> -> o*. Kann ich das anhand von Einsetzen zeigen oder argumentiere ich einfach, das x im Zustand o'' zu 0 ausgewertet wird?

Ich dachte an: o*=o''[x\x+1]=o[x\0][x\x+1]=o[x\1]=o'

Danke bereits im Vorraus.

wintermute
Erstie
Erstie
Beiträge: 15
Registriert: 6. Jul 2016 13:07

Re: Programmäquivalenz

Beitrag von wintermute » 7. Mär 2017 15:56

lukas scheidel hat geschrieben:Kann ich das anhand von Einsetzen zeigen oder argumentiere ich einfach, das x im Zustand o'' zu 0 ausgewertet wird?
Nur ganz kurz, du musst schon das Urteil \(\langle(x \oplus 1), \sigma''\rangle \Downarrow 1\) herleiten. Das wird schließlich in der Prämisse der Regel r:= benötigt. Dort möchtest du, ja \(\sigma^{*} = \sigma''[x \backslash 1]\) schließen. Anschließend verwendest du noch \(\sigma'' = \sigma[x \backslash 0]\) und erhältst dann \(\sigma''[x \backslash 1] = (\sigma[x \backslash 0])[x \backslash 1] = \sigma'\)

lukas scheidel
Neuling
Neuling
Beiträge: 3
Registriert: 7. Mär 2017 09:11

Re: Programmäquivalenz

Beitrag von lukas scheidel » 7. Mär 2017 17:47

Dass ich das herleiten muss ist klar. Deine zweite Aussage hilft mir, das wollte ich wissen.
Ich verwende also o* = o''[x\1] = (o[X\0])[X\1] = o' und erhalte die Lösung, das musste ich wissen.

Danke sehr.

Antworten

Zurück zu „Archiv“