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