I'm doing revision for a module on programming language semantics and I'm having trouble understanding the introduction of side-effects in expressions.
We assume a standard syntax for arithmetic expression, with the four usual operations, plus the unary prefix and postfix operator $\texttt{++}$, defined as in language C, applicable to variables only as in $\texttt{V++}$, and assigment statement $\texttt{V:=E}$.
We have seen how to define the denotation function $[\![\texttt{E}]\!]_{\mathrm{Exp}}$ when we have to evaluate an expression $\texttt{E}$ without side-effect, to return a value resulting from that evaluation.
In order to give a denotational semantics for expressions with side-effects, we need to change the type of the denotation function $[\![\texttt{E}]\!]_{\mathrm{Exp}}$ for expressions $\texttt{E}$, so that it returns both the value of the expression and the state as modified by the side-effects. I.e., we want to define a denotation function
$[\![\texttt{E}]\!]_{\mathrm{Exp}} : State → Int×State$
by induction on the form of expressions $\texttt{E}$. For example, in the case $\texttt{E}$ has the form $\texttt{E1+E2}$, we define:
$[\![\texttt{E1+E2}]\!]_{\mathrm{Exp}}(S) = (n_1 + n_2, S_2)$
where $(n_1, S_1) = [\![\texttt{E1}]\!]_{\mathrm{Exp}}(S)$
and $(n_2, S_2) = [\![\texttt{E2}]\!]_{\mathrm{Exp}}(S_1)$
This says first evaluate the leftmost expression $\texttt{E1}$, giving the integer value $n_1$ and updated state $S_1$, then evaluate $\texttt{E2}$ in that updated state, giving the integer value $n_2$ and updated state $S_2$; the value of the expression is $n_1 + n_2$, and evaluation has the side effect of updating the state to $S_2$.
However this does not show when side effects actually take place, and I do not know how to write the denotation function for expressions that do produce side-effects. Can you tell me how to complete the inductive definition of $[\![\texttt{E}]\!]_{\mathrm{Exp}}$, including the case where $\texttt{E}$ is of the form $\texttt{V++}$?
Then, how should one change the definition of the denotation function $[\![\texttt{V:=E}]\!]_{\mathrm{Pgm}}$ for the assignment statement, to take account of the changes in the definition of $[\![\texttt{E}]\!]_{\mathrm{Exp}}$, which it necessarily uses?
Are there other changes that would need to be made to the denotational semantics of the language?