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.