In imperative languages we have a program state... variable that can store values and have then changed.
We will need some structure in the denotational definition to deal with this... like we added the Env environments earlier to handle bindings of names to values.
We will leave out the error value stuff now that you've seen how it's done.
Syntactic Categories
I in Ident (identifiers) E in Exp (expressions) C in Comm (commands) P in Prog (full programs)Syntax BNF
E ::= 0 | 1 | I | (E1 + E2) | (E1 / E2) | let I = E1 in E2 end C ::= C1 ; C2 | if E then C1 else C2 | while E do C P ::= program (I) ; C end .Value Domains
n in Int = { ..., -2, -1, 0, 1, 2, ... } (integers) sigma in States (states, of memory)Semantic Functions
EE : Exp --> ??? CC : Comm --> States --> States PP : Prog --> Int --> IntSemantic Equations
CC [ if E then C1 else C2 ] sigma = ite( isTrue(EE [E] sigma), CC [C1] sigma, CC [C2] sigma ) (* we presume for now that EE knows how to use a state rather than an environment *) CC [ C1; C2 ] sigma = let sigma' = CC [C1] sigma in CC [C2] sigma' end (* or, CC [C1; C2] = CC [C1] o CC [C2] in functionals *) CC [[ while E do C ]] sigma = let fun p(sigma') = if isTrue(EE [E] sigma') then p(CC [C] sigma') else sigma' in p(sigma) endThis last equation is recursive (remember loops in Mills'?)