Question

1) Write a denotational semantics for do-while loop

Answer 1

1A)

Denotational semantics for do - while loop ::-

We can define the semantics for loops using either a direct or a continuation semantics. Recall that for the direct semantics, we have:

C: Command → Store⊥ → Store⊥

and we define the valuation function for a loop as follows:
C [[while B do C]] = λs. if B [[B]] then C [[while B do C]] (C [[C]] s) else s

Note that the "then" part of the if says "execute the next iteration, using the store produced by this iteration". But this is a recursive definition; what does it really mean? The answer is to use our usual trick with fixed points:
C [[while B do C]] = Y (λf.λs. if B [[B]] then f (C [[C]] s) else s)
For the continuation semantics, we have:

C: Command → Cc → Store → Store⊥

and we define the valuation function as follows:
C [[while B do C]] = λc.λs. if B [[B]] then (C [[C]] (C [[while B do C]] c) s) else (c s)

Again, we can eliminate the recursion by using Y as we did above for the direct semantics.
Of course, we need to know that the fixed points exist and are what we want.