Assignment 2 (Operational Semantics)
Due 1 February
Submit your typed homework in class
References
The assignment refers to the operational semantics of the language IMP
discussed in class. If you want a copy of the evaluation rules, please let me
know.
Equivalence
Recall the following definition for when two commands c1
and
c2
are equivalent:
c1 ~ c2 iff
forall sigma, sigma'.
< c1, sigma > --> sigma' <==> < c2, sigma > --> sigma'
Let w
be the command while b do c
for some
arbitrary boolean expression b
and command c
. Then
prove that:
w ~ if b then c;w else skip
The general idea is similar to the proof that c;skip ~ c
which
was done in class.
sabry ... cs indiana edu