fact: Fixpoint Cexec (c: com) (S: ST.t) : ST.t := match c with | SKIP => S | ASSIGN x a => ST.set x (Aeval a S) S | SEQ c1 c2 => Cexec c2 (Cexec c1 S) | IFTHENELSE b c1 c2 => ST.join (Cexec c1 (assume_test b true S)) (Cexec c2 (assume_test b false S)) | WHILE b c => assume_test b false (postfixpoint (fun X => ST.join S (Cexec c (assume_test b true X)))) end.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)