fact: Fixpoint abstract_i (i:instr)(l:ab_env) {struct i}:a_instr*option ab_env := match i with skip => (prec (to_a l) a_skip, Some l) | sequence i1 i2 => let (i'1, l') := abstract_i i1 l in match l' with None => (a_sequence i'1 (prec false_assert (mark i2)), None) | Some l' => let (i'2, l'') := abstract_i i2 l' in (a_sequence i'1 i'2, l'') end | assign x e => (prec (to_a l)(a_assign x e), Some(ab_update l x (ab_eval (ab_lookup l) e))) | while b i => match intersect_env true l b with None => (prec (to_a l)(a_while b (a_conj (a_not (a_b b))(to_a l))(mark i)), Some l) | Some l' => let (i',l'') := fp l b i (abstract_i i) in match l'' with None => (prec (to_a l) (a_while b (to_a l) i'), intersect_env false l b) | Some l'' => (prec (to_a l)(a_while b (to_a l'') i'), intersect_env false l'' b) end end end.
imports: syntax little denot Bool List String ZArith axiom