Denotational Semantics

Syntactic Categories 

  I in Ident  (identifiers)
  L in Lexp   (l-expressions)
  E in Exp    (expressions)
  C in Comm   (commands)
  P in Prog   (full programs)

Syntax BNF 

   L  ::=  I

   E  ::=  0 | 1 | I | !L | (E1 + E2) | let I = E1 in E2 end

   C  ::=  C1 ; C2
        |  if E then C1 else C2
        |  do_all_true E1: C1 , E2: C2 , ... En: Cn end
        |  new I := E in C end
        |  L := E

   P  ::=  program (I) ; C end .

Develop a full denotational definition for this language. That means adding to the syntax information above these parts: value domains, semantic functions, and semantic equations.

Much of this will be modification/combination of the examples we did in class, but you will have to create for yourself some believable denotational definition for the do_all_true loop, using these informal semantics :

The "do_all_true" loop works like this:
the body is entered, and all boolean guards Ei are evaluted before any body code is executed. For each Ei found true, the corresponding Ci will be executed, and the selected Ci parts will be executed in the order they appear in the body. Looping continues until all Ei guards evaluate to false at the beginning of some new iteration.

(Just a side note... we could imagine other related semantics... perhaps a "do_one_true" loop that might pick at random one of the true Ci parts to execute until all Ei are false... or perhaps a "do_each_true" loop that executes each true Ei part it finds, but delays evaluation of Ei until it gets to that point in the body... or perhaps other variations.)