-
Notifications
You must be signed in to change notification settings - Fork 0
/
demo.v
46 lines (41 loc) · 1.19 KB
/
demo.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
Require Import seplogic.
Example alloc_test1 :
{{ emp }}
(CCons X (ANum 1))
{{(AId X) |-> (ANum 1)}}.
Proof.
eapply rule_consequence_pre.
-apply rule_alloc.
-unfold strongerThan. intros. destruct s.
unfold s_imp. intros. simpl. intros.
unfold assn_sub, point_to. simpl.
unfold st_update. simpl.
subst. inversion H. simpl in *. subst.
rewrite h_union_emp_heap.
reflexivity.
Qed.
Example alloc_test2 :
{{ emp }}
(CSeq (CCons X (ANum 1))
(CCons Y (ANum 2)))
{{(AId X) |-> (ANum 1)**(AId Y)|->(ANum 2)}}.
Proof.
apply rule_seq with ((AId X) |-> (ANum 1)).
-eapply rule_consequence_pre.
apply rule_alloc.
+unfold strongerThan. intros. unfold s_imp.
destruct s. intros. simpl in *. intros.
unfold assn_sub. simpl. unfold st_update. simpl.
exists h. exists h'. split.
*apply disjoint_comm. assumption.
*split. ++reflexivity. ++split; assumption.
-eapply rule_consequence_pre.
+apply rule_alloc.
+unfold strongerThan. intros. destruct s.
unfold s_imp. intros. simpl. intros.
unfold assn_sub, point_to. simpl.
unfold st_update. simpl.
subst. inversion H. simpl in *. subst.
rewrite h_union_emp_heap.
reflexivity.
Qed.