CSVerifi/assertionB.v at master · PKUTCS/CSVerifi · GitHub

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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
Require Import util.
Require Import Coq.omega.Omega.
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.Lists.List.
Require Import language.
Require Import semantic.
Require Import state.
Import ListNotations.


Definition assertionB := state -> Prop.


Definition empB : assertionB :=
fun st:state => match st with
                | (stoV,stoB,stoF,hV,hB) => hB = emp_heapB
                end.


Definition point_toB (bk1 bk2:bkexp) : assertionB :=
  fun st:state =>
    match st with
    | (stoV,stoB,stoF,hV,hB) =>
        (match (bkeval stoV stoB stoF bk1),(bkeval stoV stoB stoF bk2) with
         | Some n1, Some n2 => hB = h_updateB emp_heapB n1 n2
         | _,_ => False
        end)
    end.

Notation "e1 '|=>' e2" := (point_toB e1 e2) (at level 60).


Inductive fe : Type :=
| Nil : fe
| Fi  : id -> fe
| Appbk : fe -> bkexp -> fe
| Appfe : fe -> fe -> fe.


Fixpoint feEval stoV stoB stoF feExp : option (list nat) :=
match feExp with
| Nil => Some []
| Fi fid => Some (stoF fid)
| Appbk afe abkexp => (match (feEval stoV stoB stoF afe) with
                      | Some li => (match (bkeval stoV stoB stoF abkexp) with
                                    | Some bk => Some (li ++ [bk])
                                    | None => None
                                    end)
                      | None => None
                      end)
| Appfe fe1 fe2 => (match (feEval stoV stoB stoF fe1),
                          (feEval stoV stoB stoF fe2) with
                    | Some fli1, Some fli2 => Some (fli1 ++ fli2)
                    | _,_ => None
                    end)
end.


Fixpoint allSame (li1 li2:list nat) : Prop :=
  match li1,li2 with
  | [],[] => True
  | x::xl, y::yl => (x = y) /\ (allSame xl yl)
  | _,_ => False
  end.


Definition point_toF (f:id) (feExp:fe) : assertionB :=
  fun st:state =>
    match st with
    | (stoV,stoB,stoF,hV,hB) =>
        let opfeli := (feEval stoV stoB stoF feExp) in
        let opfi := (stoF f) in
        (match opfeli, opfi with
         | Some li1, li2 => allSame li1 li2
         | _,_ => False
         end)
    end.


Definition sep_conjB (p q : assertionB) : assertionB :=
    fun st: state =>
      match st with
      | (stoV,stoB,stoF,hV,hB) =>
        exists hb1, exists hb2,
          disjointB hb1 hb2 /\ h_unionB hb1 hb2 = hB /\
          p (stoV,stoB,stoF,hV,hb1) /\ q (stoV,stoB,stoF,hV,hb2)
      end.
Notation "p '@@' q" := (sep_conjB p q) (at level 70).


Definition sep_disjB (p q: assertionB) : assertionB :=
  fun (st : state) =>
    match st with
    | (stoV,stoB,stoF,hV,hB) =>
      forall hb', disjointB hb' hB -> p (stoV,stoB,stoF, hV, hb') ->
      q (stoV,stoB,stoF,hV,h_unionB hB hb')
    end.
Notation "p '--@' q" := (sep_disjB p q) (at level 80).


Definition s_conjB (p q: assertionB) : assertionB :=
  fun (s: state) => p s /\ q s.
Notation "p '/@\' q" := (s_conjB p q) (at level 75).

Definition s_disjB (p q: assertionB) : assertionB :=
  fun (s: state) => p s \/ q s.
Notation "p '\@/' q" := (s_disjB p q) (at level 78).

Definition s_impB (p q: assertionB) : assertionB :=
  fun (s: state) => p s -> q s.
Notation "p '--->' q" := (s_impB p q) (at level 85).


Definition strongerThanB (p q: assertionB) : Prop :=
  forall s: state, s_impB p q s.
Notation "p '===>' q" := (strongerThanB p q) (at level 90).


Definition bk_eq (bk1 bk2:bkexp) : assertionB :=
  fun st:state =>
    match st with
    | (stoV,stoB,stoF,hV,hB) =>
        (match (bkeval stoV stoB stoF bk1),(bkeval stoV stoB stoF bk2) with
         | Some n1, Some n2 => n1 = n2
         | _,_ => False
        end)
    end.
Notation "e1 '=b=' e2" := (bk_eq e1 e2) (at level 60).


Definition bk_le (bk1 bk2:bkexp) : assertionB :=
  fun st:state =>
    match st with
    | (stoV,stoB,stoF,hV,hB) =>
        (match (bkeval stoV stoB stoF bk1),(bkeval stoV stoB stoF bk2) with
         | Some n1, Some n2 => n1 <= n2
         | _,_ => False
        end)
    end.
Notation "e1 '<b=' e2" := (bk_le e1 e2) (at level 60).