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