Example. Denotational semantics for the \mathcal {C} language (without loops) [dt-0004]

We shall first select a semantic domain for each syntactic class: \begin {array}{lcl} \mathbf {E} & \triangleq & \Sigma \rightarrow \mathbb {Z} \\ \mathbf {B} & \triangleq & \Sigma \rightarrow \mathbb {B} \\ \mathbf {C} & \triangleq & \Sigma \rightarrow \Sigma \\ \end {array} Here, \Sigma represents the set of states, which contains the values assigned to all variables: \Sigma \;\triangleq \; \mathcal {V} \rightarrow \mathbb {Z}

Now, we define our valuation functions, \llbracket \cdot \rrbracket _\mathcal {E} : \mathcal {E} \rightarrow \mathbf {E} : \begin {array}{lcl} \llbracket n \rrbracket _\mathcal {E}\ \sigma & = & n \\ \llbracket x \rrbracket _\mathcal {E}\ \sigma & = & \sigma (x) \\ \llbracket e_1 + e_2 \rrbracket _\mathcal {E}\ \sigma & = & \llbracket e_1 \rrbracket _\mathcal {E}\ \sigma + \llbracket e_2 \rrbracket _\mathcal {E}\ \sigma \\ \llbracket e_1 - e_2 \rrbracket _\mathcal {E}\ \sigma & = & \llbracket e_1 \rrbracket _\mathcal {E}\ \sigma - \llbracket e_2 \rrbracket _\mathcal {E}\ \sigma \\[2em] \end {array} and \llbracket \cdot \rrbracket _\mathcal {B} : \mathcal {B} \rightarrow \mathbf {B}: \begin {array}{lcl} \llbracket \mathsf {false} \rrbracket _\mathcal {B}\ \sigma & = & \mathit {F} \\ \llbracket \mathsf {true} \rrbracket _\mathcal {B}\ \sigma & = & \mathit {T} \\ \llbracket \neg b \rrbracket _\mathcal {B}\ \sigma & = & \begin {cases}\mathit {F} & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \mathit {T} & \text {otherwise} \end {cases} \\[1.1em] \llbracket e_1 = e_2 \rrbracket _\mathcal {B}\ \sigma & = & \begin {cases}\mathit {T} & \text {if}\ \llbracket e_1 \rrbracket _\mathcal {E}\ \sigma = \llbracket e_2 \rrbracket _\mathcal {E}\ \sigma \\ \mathit {F} & \text {otherwise} \end {cases} \end {array} and \llbracket \cdot \rrbracket _\mathcal {C} : \mathcal {C} \rightarrow \mathbf {C}: \begin {array}{lcl} \llbracket \mathsf {skip} \rrbracket _\mathcal {C}\ \sigma & = & \sigma \\ \llbracket x := e \rrbracket _\mathcal {C}\ \sigma & = & \sigma \left (x \mapsto \llbracket e \rrbracket _\mathcal {E}\right ) \\ \llbracket c_1 ; c_2 \rrbracket _\mathcal {C}\ \sigma & = & \llbracket c_2 \rrbracket _\mathcal {C}\ \left (\llbracket c_1 \rrbracket _\mathcal {C}\ \sigma \right ) \\[0.3em] \llbracket \textsf {if}\ b\ \textsf {then}\ c_1\ \textsf {else}\ c_2 \rrbracket _\mathcal {C}\ \sigma & = & \begin {cases}\llbracket c_1 \rrbracket _\mathcal {C}\ \sigma & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \llbracket c_2 \rrbracket _\mathcal {C}\ \sigma & \text {otherwise} \end {cases} \end {array}