Denotational Semantics
The text describes a denotational semantics for the simple imperative language given by the grammar
P ::= x := e | P1; P2 | if e then P1 else P2 | while e do P.
Each program denotes a function from states to states, in which a state is afunction from variables to values.
(a) Calculate the meaning C[[ x := 1; x := x + 1;]](s0) in approximately the same detail as that of the examples given in the text, where s0 = λv ∈ variables. 0, giving every variable the value 0.
(b) Denotational semantics is sometimes used to justify ways of reasoning about programs. Write a few sentences, referring to your calculation in part (a), explaining why C[[x := 1; x := x + 1;]](s) = C[[x := 2;]](s) for every state s.