fact: Fixpoint cinterp (fuel: nat) (c: com) (s: store) : option store := match fuel with | O => None | S n => match c with | SKIP => Some s | ASSIGN x a => Some (update x (aeval a s) s) | SEQ c1 c2 => bind (cinterp n c1 s) (cinterp n c2) | IFTHENELSE b c1 c2 => cinterp n (if beval b s then c1 else c2) s | WHILE b c1 => if beval b s then bind (cinterp n c1 s) (cinterp n (WHILE b c1)) else Some s end end.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)