fact: CoFixpoint cinterp (c: com) (s: store) : mon store := match c with | SKIP => Ret s | ASSIGN x a => Ret (update x (aeval a s) s) | SEQ c1 c2 => Bind (cinterp c1 s) (cinterp c2) | IFTHENELSE b c1 c2 => Later (cinterp (if beval b s then c1 else c2) s) | WHILE b c => if beval b s then Bind (cinterp c s) (cinterp (WHILE b c)) else Ret s end.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)