S00-03 Formális szemantika

Tartalom

  1. Formális kontra informális definíciók, a formális szemantika alkalmazási területei, a szemantikamegadási módszerek áttekintése
  2. Mesterséges nyelvek konkrét és absztrakt szintaxisa
  3. Statikus és dinamikus szemantika
  4. Attribútum-grammatikák és alkalmazásaik
  5. Alapvető imperatív nyelvi elemek strukturális és természetes műveletei, illetve leíró szemantikája, hasonlóságok és különbségek
  6. Kompozicionális és strukturális indukció
  7. Rekurzív függvények és ciklusok leíró szemantikája, fixpont-elmélet
  8. További források

1. Formális kontra informális definíciók, a formális szemantika alkalmazási területei, a szemantikamegadási módszerek áttekintése

Bevezetés

Formális szemantika: programok jelentésének

Formális szemantika előnyei

  1. Alapvető dokumentáció
  2. Félreérthető elemek feltárása
  3. Precíz jelentésfogalom \(\Longrightarrow\) bizonyíthatóság

Három fő komponens

  1. Szintaxis
  2. Szemantika
  3. Pragmatika

Megközelítései

  1. Attribútum grammatikákkal
  2. Operációs (műveleti) szemantikával
  3. Denotációs (leíró) szemantikával
  4. Axiomatikus szemantikával

2. Mesterséges nyelvek konkrét és absztrakt szintaxisa

Konkrét szintaxis

<assignment> ::= 'LET' <variable> ':=' <expression> ';'

Absztrakt szintaxis

\[A :== assignment(V, E)\]

ahol

3. Statikus és dinamikus szemantika

Szintaxisnak nem minden elemét lehet környezetfüggetlen grammatikával kifejezni

Statikus szemantika

Dinamikus szemantika

Példák

4. Attribútum-grammatikák és alkalmazásaik

Környezetfüggetlen grammatika

\[G = (T, N, P, S)\]

ahol

Mitől környezetfüggetlen egy környezetfüggetlen grammatika?

Attribútum grammatika

Attribútum grammatika formálisan

Hogy csinálunk attribútum grammatikát?

\[AG = (G, A, R, C)\]

ahol

Attribútumok

Jelölések:

Attribútumok típusai

Szintetizált

Örökölt

Egyéb tudnivalók az attribútumok típusairól:

Jól definiált attribúm grammatika (Well-defined Attributum Grammatics, WAG)

5. Alapvető imperatív nyelvi elemek strukturális és természetes műveleti, illetve leíró szemantikája, hasonlóságok és különbségek

Állapotok a szemantikában

Ebből: \((s[y \rightarrow v])[x]\)

(Egy másik formalizáltabb felírásban ami nincs a jegyzetben, de annak jó aki így könnyebben megtanulja:)

\[ (s[y \rightarrow v])[x] = \begin{cases} v' &\mbox{ha } x = y' \\ s[x] & \mbox{egyébként} \end{cases} \]

Strukturális operációs szemantika

Átmenet

Skip strukturális operációs szemantikája

\[\begin{align*} \cline{1-2} & \langle \textbf{skip}, s \rangle \Longrightarrow s \end{align*}\]

Értékadás strukturális operációs szemantikája

\[\begin{align*} \cline{1-2} & \langle x := a, s \rangle \Longrightarrow s[x \rightarrow A [\![a]\!] s] \end{align*}\]

Szekvencia strukturális operációs szemantikája

Köztes állapot:

\[\begin{align*} & \langle S_1, s \rangle \Longrightarrow \langle S'_1, s' \rangle \\ \cline{1-2} & \langle S_1; S_2, s \rangle \Longrightarrow \langle S'_1; S_2, s' \rangle \end{align*}\]

Végállapot:

\[\begin{align*} & \langle S_1, s \rangle \Longrightarrow s' \\ \cline{1-2} & \langle S_1; S_2, s \rangle \Longrightarrow \langle S_2, s' \rangle \end{align*}\]

Elágazás strukturális operációs szemantikája

Ha igaz:

\[\begin{align*} \cline{1-2} && B[\![b]\!]s = tt \\ & \langle \textbf{if}\ b\ \textbf{then}\ S_1\ \textbf{else}\ S_2, s \rangle \Longrightarrow \langle S_1, s \rangle \end{align*}\]

Ha hamis:

\[\begin{align*} \cline{1-2} && B[\![b]\!]s = ff \\ & \langle \textbf{if}\ b\ \textbf{then}\ S_1\ \textbf{else}\ S_2, s \rangle \Longrightarrow \langle S_2, s \rangle \end{align*}\]

Ciklus strukturális operációs szemantikája

\[\begin{align*} \cline{1-2} & \langle \textbf{while}\ b\ \textbf{do}\ S, s \rangle \Longrightarrow \langle \textbf{if}\ b\ \textbf{then}\ (S;\ \textbf{while}\ b\ \textbf{do}\ S)\ \textbf{else}\ \textbf{skip}, s \rangle \end{align*}\]

Szemantikus ekvivalencia (strukturális operációs szemantika)

Szemantikus ekvivalencia általában: megadja, hogy két utasítás jelentése megegyezik-e

Strukturális operációs szemantika esetén

\(S_1\) és \(S_2\) szemantikusan ekvivalensek (\(S_1 \equiv S_2\)), ha minden s állapotra

ahol c termináló vagy zsákutca konfiguráció

Szemantikus függvény (strukturális operációs szemantika)

\[S_{SOS} : Stm \rightarrow (State \hookrightarrow State)\]

\[ S_{SOS}[\![S]\!]s = \begin{cases} s' &\mbox{ha } \langle S, s \rangle \Longrightarrow ^* s' \\ undefined & \mbox{egyébként} \end{cases} \]

Természetes operációs szemantika

S utasítás végrehajtása \(s'\) állapotot eredményezi

Következtetési szabályai:

Skip természetes operációs szemantikája

\[\begin{align*} \cline{1-2} & \langle \textbf{skip}, s \rangle \rightarrow s \end{align*}\]

Értékadás természetes operációs szemantikája

\[\begin{align*} \cline{1-2} & \langle x := a, s \rangle \rightarrow s[x \rightarrow A [\![a]\!] s] \end{align*}\]

Szekvencia természetes operációs szemantikája

\[\begin{align*} & \langle S_1, s \rangle \rightarrow s' \qquad \langle S_2, s' \rangle \rightarrow s'' \\ \cline{1-2} & \langle S_1; S_2, s \rangle \rightarrow \langle s'' \rangle \end{align*}\]

Elágazás természetes operációs szemantikája

\[\begin{align*} & \langle S_1, s \rangle \rightarrow s' \\ \cline{1-2} && B[\![b]\!]s = tt \\ & \langle \textbf{if}\ b\ \textbf{then}\ S_1\ \textbf{else}\ S_2, s \rangle \rightarrow s' \end{align*}\] \[\begin{align*} & \langle S_2, s \rangle \rightarrow s' \\ \cline{1-2} && B[\![b]\!]s = ff \\ & \langle \textbf{if}\ b\ \textbf{then}\ S_1\ \textbf{else}\ S_2, s \rangle \rightarrow s' \end{align*}\]

Ciklus természetes operációs szemantikája

\[\begin{align*} & \langle S, s \rangle \rightarrow s' \qquad \langle \textbf{while}\ b\ \textbf{do}\ S, s' \rangle \rightarrow s'' \\ \cline{1-2} && B[\![b]\!]s = tt \\ & \langle \textbf{while}\ b\ \textbf{do}\ S, s \rangle \rightarrow s'' \end{align*}\] \[\begin{align*} \cline{1-2} && B[\![b]\!]s = ff \\ & \langle \textbf{while}\ b\ \textbf{do}\ S, s \rangle \rightarrow s \end{align*}\]

Szemantikus ekvivalencia (természetes operációs szemantika)

\(S_1\) és \(S_2\) szemantikusan ekvivalensek, ha minden s és s' állapotra

Szemantikus függvény (természetes operációs szemantika)

\[S_{NS} : Stm \rightarrow (State \hookrightarrow State)\]

\[ S_{NS}[\![S]\!]s = \begin{cases} s' &\mbox{ha } \langle S, s \rangle \rightarrow s' \\ undefined & \mbox{egyébként} \end{cases} \]

Denotációs szemantika

\[S_{ds} : Stm \rightarrow (State \rightarrow State)\]

Imperatív nyelvi elemek denotációs szemantikája

\[ \begin{aligned} S_{ds}[\![\textbf{skip}]\!] = id_{State} \\ S_{ds}[\![x := a]\!]s = s[x \mapsto A[\![a]\!]s] \\ S_{ds}[\![S_1; S_2]\!] = S_{ds}[\![S_2]\!] \circ S_{ds}[\![S_1]\!] \\ S_{ds}[\![\textbf{if}\ b\ \textbf{then}\ S_1\ \textbf{else}\ S_2]\!] = cond(B[\![b]\!], S_{ds}[\![S_1]\!], S_{ds}[\![S_2]\!]) \\ S_{ds}[\![\textbf{while}\ b\ \textbf{do}\ S]\!] = FIX\ F\ \\ \qquad where\ F\ g\ = cond(B[\![b]\!], g \circ S_{ds}[\![S]\!], id_{State}) \end{aligned} \]

6. Kompozicionális és strukturális indukció

Kompozicionalitás

Mi bizonyítható a strukturális indukcióval?

  1. A definíció teljes
  2. A szemantika konzisztens
  3. A kifejezésekre definiált operációs és denotációs szemantika ekvivalens

7. Rekurzív függvények és ciklusok leíró szemantikája, fixpont-elmélet

\[S_{ds}[\![\textbf{while}\ b\ \textbf{do}\ S]\!] = cond(B[\![b]\!], S_{ds}[\![\textbf{while}\ b\ \textbf{do}\ S]\!] \circ S_{ds}[\![S]\!], id_{State})\] \[g = cond(B[\![b]\!], g \circ S_{ds}[\![S]\!], id_{State})\]

Megoldás: \(S_{ds}[\![\textbf{while}\ b\ \textbf{do}\ S]\!]\) jobb oldalát alakítsuk át magasabbrendű függvénnyé, aminek paramétere g függvény!

\[F : (State \hookrightarrow State) \rightarrow (State \hookrightarrow State)\] \[F g = cond(B[\![b]\!], g \circ S_{ds}[\![S]\!], id_{State}) = g\]

Formula megoldásait tehát F fixpontjának kiszámításával kapjuk meg:

\[S_{ds}[\![\textbf{while}\ b\ \textbf{do}\ S]\!] = FIX\ F\]

8. További források