Using notation similar to Backus-Naur Form (BNF): \begin {array}{lcl} \mathcal {E} & \Coloneqq & n \mid x \mid \mathcal {E}_1 + \mathcal {E}_2 \mid \mathcal {E}_1 - \mathcal {E}_2\\ \mathcal {B} & \Coloneqq & \mathsf {false} \mid \mathsf {true} \mid \neg \mathcal {B} \mid \mathcal {E}_1 = \mathcal {E}_2\\ \mathcal {C} & \Coloneqq & \mathsf {skip} \mid x := \mathcal {E} \mid \mathcal {C}_1 ; \mathcal {C}_2 \mid \mathsf {if}\ \mathcal {B}\ \mathsf {then}\ \mathcal {C}_1\ \mathsf {else}\ \mathcal {C}_2\\ x & \in & \mathcal {V}\; \textit {(variables)}\\ n & \in & \mathbb {N} \end {array}

A denotational semantics consists of, for each syntactic class \mathcal {X} in a language:

1. A semantic domain D which can be any set of mathematical objects (although, as we will see later, it is helpful if it obeys certain properties).
2. A valuation function \llbracket \cdot \rrbracket : \mathcal {X} \rightarrow D. We require that this function be a homomorphism, that is that it is compositional. This means that the valuation (or denotation) of an expression should be made from the denotation of its components. In other words, for each syntactic constructor C(e_1,e_2,\dots ), we should have a mathematical operation f(x_1,x_2,\dots ) such that the denotation of C can be defined as: \llbracket C(e_1, e_2, \dots ) \rrbracket = f(\llbracket e_1 \rrbracket , \llbracket e_2 \rrbracket , \dots )

The choices of semantic domain and valuation function are, essentially, arbitrary: we choose objects that reflect those aspects of our programs that we are interested in. For most of the simple languages we will examine, we are only concerned with the results of the computation, which is a semantics suitable for reasoning about program behaviour and correctness. However, there also exist denotational cost models that compositionally assign a measure of program performance to syntax. This measure is just another kind of denotational semantics.

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}