Seite 1 von 1

Programmäquivalenz

Verfasst: 7. Mär 2017 09:19
von lukas scheidel
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.

Re: Programmäquivalenz

Verfasst: 7. Mär 2017 15:56
von wintermute
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'\)

Re: Programmäquivalenz

Verfasst: 7. Mär 2017 17:47
von lukas scheidel
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.