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
|
(* This file was originally generated by why.
It can be modified; only the generated parts will be overwritten. *)
Require Export abs_spec_why.
(* Why obligation from file "/home/jcf/soft/why/examples-c/tutorial/abs.c", line 5, characters 6-8: *)
(*Why goal*) Lemma abs1_impl_po_1 :
forall (p: (pointer global)),
forall (alloc: alloc_table),
(valid alloc p).
Proof.
intuition.
Admitted.
(* Why obligation from file "/home/jcf/soft/why/examples-c/tutorial/abs.c", line 3, characters 12-19: *)
(*Why goal*) Lemma abs1_impl_po_2 :
forall (p: (pointer global)),
forall (alloc: alloc_table),
forall (intM_global: (memory Z global)),
forall (HW_1: (valid alloc p)),
forall (result: Z),
forall (HW_2: result = (acc intM_global p)),
forall (HW_3: result < 0),
forall (HW_4: (valid alloc p)),
forall (result0: Z),
forall (HW_5: result0 = (acc intM_global p)),
forall (HW_6: (valid alloc p)),
forall (intM_global0: (memory Z global)),
forall (HW_7: intM_global0 = (upd intM_global p (Zopp result0))),
(* CADUCEUS_1 *) (acc intM_global0 p) >= 0.
Proof.
intuition.
subst; caduceus.
Save.
(* Why obligation from file "/home/jcf/soft/why/examples-c/tutorial/abs.c", line 3, characters 12-19: *)
(*Why goal*) Lemma abs1_impl_po_3 :
forall (p: (pointer global)),
forall (alloc: alloc_table),
forall (intM_global: (memory Z global)),
forall (HW_1: (valid alloc p)),
forall (result: Z),
forall (HW_2: result = (acc intM_global p)),
forall (HW_8: result >= 0),
(* CADUCEUS_1 *) (acc intM_global p) >= 0.
Proof.
intuition.
Save.
(* Why obligation from file "/home/jcf/soft/why/examples-c/tutorial/abs.c", line 9, characters 12-19: *)
(*Why goal*) Lemma abs2_impl_po_1 :
forall (p: (pointer global)),
forall (alloc: alloc_table),
forall (intM_global: (memory Z global)),
forall (HW_1: (* CADUCEUS_5 *) (valid alloc p)),
forall (HW_2: (valid alloc p)),
forall (result: Z),
forall (HW_3: result = (acc intM_global p)),
forall (HW_4: result < 0),
forall (HW_5: (valid alloc p)),
forall (result0: Z),
forall (HW_6: result0 = (acc intM_global p)),
forall (HW_7: (valid alloc p)),
forall (intM_global0: (memory Z global)),
forall (HW_8: intM_global0 = (upd intM_global p (Zopp result0))),
(* CADUCEUS_6 *) (acc intM_global0 p) >= 0.
Proof.
intuition.
subst intM_global0.
caduceus.
Save.
(* Why obligation from file "/home/jcf/soft/why/examples-c/tutorial/abs.c", line 9, characters 12-19: *)
(*Why goal*) Lemma abs2_impl_po_2 :
forall (p: (pointer global)),
forall (alloc: alloc_table),
forall (intM_global: (memory Z global)),
forall (HW_1: (* CADUCEUS_5 *) (valid alloc p)),
forall (HW_2: (valid alloc p)),
forall (result: Z),
forall (HW_3: result = (acc intM_global p)),
forall (HW_9: result >= 0),
(* CADUCEUS_6 *) (acc intM_global p) >= 0.
Proof.
intuition.
Save.
|
