fact: Fixpoint vcg (i:a_instr)(post : assert) {struct i} : list condition := match i with prec a i => c_imp a (pc i post)::vcg i post | a_skip => nil | a_assign _ _ => nil | a_sequence i1 i2 => vcg i2 post ++ vcg i1 (pc i2 post) | a_while e a i => c_imp (a_conj (a_not (a_b e)) a) post :: c_imp (a_conj (a_b e) a) (pc i a) :: vcg i a end.
imports: syntax little denot Bool List String ZArith