Sémantika výrazov

Krok 1

V tomto predmete pracujeme s abstraktným jazykom Jane. Tento jazyk obsahuje základné syntaktické konštrukcie typické pre imperatívne jazyky – priradenie hodnoty premennej (zmena obsahu pamäte), vetvenie (dvojcestné, na základe logickej podmienky), cyklus (prefixný s logickou podmienkou). Jazyk obshauje tiež aritmetické výrazy s celočíselnými hodnotami a boolovské výrazy s logickými hodnotami.

Aritmetické výrazy konštruujeme z prvkov syntaktickej oblasti aritmetických výrazov $\mathbf{Expr}$. Ich syntax je nasledovná: $$ e ::= ~n~|~x~|~e~+ ~e~|~e~-~e~|~e~*~e~|~(e),$$ pričom $e \in \mathbf{Expr}$.

Podobne konštruujeme aj boolovské výrazy z prvkov syntaktickej oblasti boolovských výrazov $\mathbf{Bexpr}$. Ich syntax je nasledovná: $$ b ::= ~\mathtt{true}~|~\mathtt{false}~|~e~=~e~|~e~\leq~e~|~\neg~b~|~b~\wedge ~b~|~(b), $$ pričom $b \in \mathbf{Bexpr}$.

Syntax a sémantiku aritmetických aj boolovských výrazov je možné rozšíriť pridaním nových prvkov. Pri definovaní sémantiky obvykle vychádzame zo známych matematických pravidiel. S rozšírením syntaxe a sémantiky sa oboznámime v kroku 4.

Krok 2

Aby sme mohli vyjadriť sémantiku (význam) aritmetických výrazov, musíme zaviesť pojem stavu pamäte. Stav je prvkom sémantickej oblasti stavov $\mathbf{State}$ a definujeme ho ako funkciu, ktorá premennej priradí jej hodnotu: $$s : \mathbf{Var} \rightarrow \mathbf{Z}.$$

Pri vyhodnocovaní výrazov má stav len pasívnu rolu (nemení sa). Ak napr. premenná $x$ má v stave $s_{1}$ hodnotu $\mathbf{14}$, potom túto skutočnosť zapisujeme $$ s_{1}~x = \mathbf{14}$$ alebo $$ s_{1} = \left[x \mapsto \mathbf{14}\right].$$

Sémantiku výrazov môžeme definovať len pre syntakticky správne výrazy. To dosiahneme definovaním príslušnej sémantickej funkcie. Sémantická funkcia pre aritmetické výrazy je funkciou dvoch argumentov – výrazu a stavu:

$$\mathscr{E}: \mathbf{Expr} \rightarrow \mathbf{State}\rightarrow \mathbf{Z}.$$

Ak predpokladáme existenciu funkcie $\mathscr{N}$ (Cvičenie 1), ktorá definuje význam numerálov, potom môžeme definovať funkciu $\mathscr{E}$ pre jednotlivé tvary aritmetických výrazov pomocou sémantických rovností v nasledujúcej tabuľke:

$$ \begin{array}{l} \mathscr{E} [\![ n ]\!]~s = \mathscr{N} [\![ n ]\!] \\ \mathscr{E} [\![ x ]\!]~s = s~x \\ \mathscr{E} [\![ e_{1} + e_{2} ]\!]~s = \mathscr{E} [\![ e_{1} ]\!]~s \oplus \mathscr{E} [\![ e_{2} ]\!]~s\\ \mathscr{E} [\![ e_{1} - e_{2} ]\!]~s = \mathscr{E} [\![ e_{1} ]\!]~s \ominus \mathscr{E} [\![ e_{2} ]\!]~s\\ \mathscr{E} [\![ e_{1} * e_{2} ]\!]~s = \mathscr{E} [\![ e_{1} ]\!]~s \otimes \mathscr{E} [\![ e_{2} ]\!]~s\\ \mathscr{E} [\![ (e) ]\!]~s = (\mathscr{E} [\![ e ]\!]~s) \\ \end{array} $$

Sémantickú funkciu aplikujeme postupne.

Krok 3

Boolovské (logické) výrazy v jazyku Jane (a vo väčšine skutočných programovacích jazykov) slúžia na zistenie pravdivostnej hodnoty podmienky v podmieňovacom príkaze alebo v príkaze cyklu. Významom boolovských výrazov je pravdivostná hodnota. Pre tieto hodnoty definujeme sémantickú oblasť $$\mathbf{B} = \{ \mathbf{tt}, \mathbf{ff} \},$$ pričom

• $\mathbf{tt}$ bude označovať pravdivosť,
• $\mathbf{ff}$ bude označovať nepravdivosť.

Definujeme sémantickú funkciu $\mathscr{B}$ pre boolovské výrazy: $$\mathscr{B}: \mathbf{Bexp} \rightarrow \mathbf{State} \rightarrow \mathbf{B}.$$ Funkciu $\mathscr{B}$ pre jednotlivé tvary boolovských výrazov definujeme pomocou sémantických rovností v nasledujúcej tabuľke:

$$ \begin{array}{ll} \mathscr{B} [\![ \mathtt{true} ]\!]~s = & \mathbf{tt}, \\ & \\ \mathscr{B} [\![ \mathtt{false} ]\!]~s = & \mathbf{ff}, \\ & \\ \mathscr{B} [\![ e_{1} = e_{2} ]\!]~s = & \mathbf{tt}, \text{ ak } \mathscr{E} [\![ e_{1} ]\!]~s = \mathscr{E} [\![ e_{2} ]\!]~s, \\ & \mathbf{ff}, \text{ ak } \mathscr{E} [\![ e_{1} ]\!]~s \neq \mathscr{E} [\![ e_{2} ]\!]~s, \\ &\\ \mathscr{B} [\![ e_{1} \leq e_{2} ]\!]~s = & \mathbf{tt}, \text{ ak } \mathscr{E} [\![ e_{1} ]\!]~s \leq \mathscr{E} [\![ e_{2} ]\!]~s, \\ & \mathbf{ff}, \text{ ak } \mathscr{E} [\![ e_{1} ]\!]~s \mathscr{E} [\![ e_{2} ]\!]~s, \\ &\\ \mathscr{B} [\![ \neg b ]\!]~s = & \mathbf{tt}, \text{ ak } \mathscr{B} [\![ \neg b ]\!]~s = \mathbf{ff}, \\ & \mathbf{ff}, \text{ ak } \mathscr{B} [\![ \neg b ]\!]~s = \mathbf{tt}, \\ & \\ \mathscr{B} [\![ b_{1} \wedge b_{2} ]\!]~s = & \mathbf{tt}, \text{ ak } \mathscr{B} [\![ b_{1} ]\!]~s = \mathbf{tt} \text{ a } \mathscr{B} [\![ b_{2} ]\!]~s = \mathbf{tt}, \\ & \mathbf{ff}, \text{ ak } \mathscr{B} [\![ b_{1} ]\!]~s = \mathbf{ff} \text{ alebo } \mathscr{B} [\![ b_{2} ]\!]~s = \mathbf{ff}, \\ &\\ \mathscr{B} [\![ (b) ]\!]~s = & (\mathscr{B} [\![ b ]\!]~s). \\ & \\ \end{array} $$

Pretože boolovské výrazy môžu obsahovať aritmetické výrazy, ktorých hodnota môže závisieť od aktuálnych hodnôt premenných, opäť musíme uvažovať stavy. Sémantické rovnosti pre jednotlivé alternatívy produkčného pravidla definujú význam boolovského výrazu v stave $s$.

Krok 4

Syntax aritmetických výrazov a boolovských výrazov možno podľa potreby kedykoľvek rozšíriť pridaním nových prvkov do produkčného pravidla. K takto pridaným prvkom je potrebné definovať ich význam. Pri definícii využívame obvyklé postupy a štandardné matematické vlastnosti.

Podobne postupujeme aj pri boolovských výrazoch.