Formal Semantics of Programming Languages
Exercise #3
Due: 10/4/03


1.
(a) prove the referential transparency property for IMP expressions, i.e.,
if for every X \in Use(a): s(X) = s'(X) then <a,s> -> n <=> <a,s'> -> n.
Where Use(a) = set of variables used in the expression a.
(b) Suppose IMP is extended with new expressions of the forms X++ and ++X which have the side
effect of updating the value of a variable X. Extend the definition of IMP's operational semantics
(as derivation rules) to include these new expression forms.

2.
Suppose the syntax of IMP is extended with the new command repeat C until B
(i.e., C is executed repeatedly until B becomes true)
(a) Extend the definition of IMP's operational semantics (as derivation rules) to include the repeat command.
No axiom or rule can make use of a while loop.
(b) Extend the definition of IMP's denotational semantics to include the repeat command.
No axiom or rule can make use of a while loop.
(c) To check your extended definition of the IMP operational semantics prove that
repeat C until B ~ C; while B do C
(by induction on the length of derivation)
(d) prove the above equivalence using denotational semantics.

3.
Suppose we want to add labels and a 'goto label' statement to IMP. Explain what
are the difficulties in defining the denotational semantics for the goto statement.
Note: you just have to provide a sufficient explanation of the problem, you are not
required to define such denotational semantics.

4.
Solve ex. 5.13 of the text book (page 73).