Require syntax.
Require Lattice.
Require func.
Require StackLattice.
Require AbVal.
Require FiniteSet.
Require analysis.
Require correct.
Require construct_analyzer.
Require rel_correct.
Require semantic.
Theorem analyzer_verifyAllFlow : (P:Program)
(verifyAllFlow P (analyzer P)).
Intros.
Apply fix_apply_list_func1.
Elim (lfp_is_lifp ? (LatAbState P) (Flow_func P) (Flow_func_monotone P));
Intros.
Unfold analyzer; Auto.
Qed.
Theorem analyzer_least_verifyAllFlow : (P:Program)
(AbS:(AbState P))
(verifyAllFlow P AbS) ->
(order (LatAbState P) (analyzer P) AbS).
Intros.
Elim (lfp_is_lifp ? (LatAbState P) (Flow_func P) (Flow_func_monotone P));
Intros.
Unfold analyzer.
Apply H1.
Apply fix_apply_list_func2; Auto.
Qed.
Theorem analyzer_list_verifyAllFlow : (P:Program)
(verifyAllFlow P (analyzer_list P)).
Intros.
Apply fix_apply_list_collect1.
Intros.
Elim (lfp_list_is_lifp ? (LatAbState P)
(collect_func P)
(collect_func_monotone P));
Intros.
Unfold analyzer_list; Auto.
Qed.
Theorem analyzer_list_least_verifyAllFlow : (P:Program)
(AbS:(AbState P))
(verifyAllFlow P AbS) ->
(order (LatAbState P) (analyzer_list P) AbS).
Intros.
Elim (lfp_list_is_lifp ? (LatAbState P)
(collect_func P)
(collect_func_monotone P));
Intros.
Unfold analyzer_list.
Apply H1.
Apply fix_apply_list_collect2; Auto.
Qed.
Theorem analyzer_correct :
(P : Program ; st : State)
(reachable_State P st) ->
(R_State P st (analyzer P)).
Intros.
Apply SubjectReduction.
Apply analyzer_verifyAllFlow.
Assumption.
Qed.
Theorem analyze :
(P:Program){AbS:(AbState P) |
(st:State) (reachable_State P st) -> (R_State P st AbS)}.
Intros P.
Exists (analyzer P).
Apply analyzer_correct.
Qed.
Extraction Inline iter_until_fix_f fix Fix_F.
Extraction"Caml/analyse.ml" analyzer analyzer_list.