-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCorrect.v
128 lines (122 loc) · 3.95 KB
/
Correct.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
From Rela Require Import Vcg.
From Rela Require Import Hoare_Triple.
From Rela Require Import Com.
From Rela Require Import Aexp.
From Rela Require Import Bexp.
From Rela Require Import Sigma.
From Rela Require Import Loc.
Import Why3_Set.
Import Assn_b.
From Coq Require Import Lists.List.
Import ListNotations.
(** Proof that one can use a verification condition generator to proof Hoare Triples **)
Lemma correct_c :
forall p cl ps l,
forall (P :precondition) (Q: postcondition),
(forall m, P m -> tc' p m l cl) ->
(forall m, P m -> tc p m l cl (fun m' _ => Q m' m)) ->
hoare_triple_ctx cl ps P Q p.
Proof.
unfold hoare_triple_ctx.
intros p cl ps.
induction p.
* unfold hoare_triple. intros. eapply H0. apply H2. inversion H3;subst. reflexivity.
* unfold hoare_triple. intros. eapply H0. apply H2. inversion H3;subst. reflexivity.
* unfold hoare_triple. intros. eapply H0. apply H2. inversion H3;subst. reflexivity.
* unfold hoare_triple. intros. eapply H0. apply H2.
apply H. apply H2. inversion H3;subst. reflexivity.
* intros l P Q Htc' Htc Hproc. eapply seq_hoare_triple.
apply (IHp1 l).
- apply Htc'.
- intros.
apply (consequence_tc_suite _ _ _ _
(fun m' h => tc' p2 m' h cl /\ tc p2 m' h cl (fun m'' _ => Q m'' m))).
+ intros s l0 H0 s''.
generalize dependent H0.
generalize dependent s''.
generalize dependent s.
apply (IHp2 l0 ).
** intros. apply H0.
** intros. apply H0.
** apply Hproc.
+ apply tc_split.
** apply Htc'. apply H.
** apply Htc. apply H.
- apply Hproc.
* intros l P Q Htc' Htc Hproc. apply if_hoare_triple.
+ apply (IHp1 l).
- intros. apply Htc'. apply H. apply bexp_eval_true. apply H.
- intros. simpl in Htc. destruct H. specialize (Htc m H). destruct Htc.
apply H1. apply bexp_eval_true. assumption.
- assumption.
+ apply (IHp2 l).
- intros. apply Htc'. apply H. destruct H. apply bexp_eval_false in H0. apply H0.
- intros. simpl in H. destruct H. specialize (Htc m H). destruct Htc.
apply H2. apply bexp_eval_false. assumption.
- assumption.
* intros l P Q Htc' Htc.
specialize (IHp l (fun s => inv (s :: l) /\ beval s b = true) (fun s _ => inv (s :: l))).
intros Hproc s s' Pre Heval.
specialize (Htc' s Pre).
simpl in Htc'.
destruct Htc'.
specialize (Htc s Pre H).
assert (H1 : inv (s' :: l) /\ beval s' b = false -> Q s' s).
{ intros. apply Htc. apply H1. apply H1. }
apply H1.
generalize Heval.
generalize H.
apply while_triple.
destruct H0.
apply IHp.
** intros.
apply H0.
destruct H3.
apply bexp_eval_true in H4.
assumption.
apply H3.
** intros.
apply H2.
destruct H3.
apply bexp_eval_true in H4.
assumption.
apply H3.
** assumption.
* intros l P Q Htc' Htc Hproc.
intros s s' Pre Heval.
specialize (Htc' s Pre).
specialize (Htc s Pre).
apply Htc; [apply Htc' | ].
generalize Heval.
generalize dependent Htc'.
apply Hproc.
Qed.
(** Proof that one can use a verification condition
generator to proof procedure contract **)
Lemma correct_proc :
forall cl ps,
tc_p ps cl ->
hoare_triple_proc_ctx cl ps.
Proof.
intros cl ps Htc.
unfold hoare_triple_proc_ctx.
intros.
apply correct_c with Vcg.empty_history.
* apply Htc.
* apply Htc.
Qed.
(** Proof that one can use a verification condition
generator for modular Hoare triple verification **)
Theorem correct :
forall (c: com) (cl: Phi.phi) (ps: Psi.psi) (l : history),
forall (P :precondition) (Q: postcondition),
tc_p ps cl ->
(forall m, P m -> tc' c m l cl) ->
(forall m, P m -> tc c m l cl (fun m' _ => Q m' m)) ->
hoare_triple P Q c ps.
Proof.
intros.
apply recursion_hoare_triple with cl.
* apply correct_proc. assumption.
* apply correct_c with l. all: try assumption.
Qed.