-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathdl.html
91 lines (86 loc) · 14.4 KB
/
dl.html
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
<h1>Why3 Proof Results for Project "dl"</h1>
<h2><span style="color:#008000">Theory "dl.Exprs_Updates": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="1">Obligations</td><td text-rotation="90">CVC4 1.8</td><td text-rotation="90">Z3 4.8.6</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for sizeU_pos</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for sizeE_pos</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for eval_upd_dom</td><td style="background-color:#C0FFC0">0.22</td><td style="background-color:#E0E0E0">---</td></tr>
</table>
<h2><span style="color:#008000">Theory "dl.Programs": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="1">Obligations</td><td text-rotation="90">Alt-Ergo 2.4.0</td><td text-rotation="90">Z3 4.8.6</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for size</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">IfSeqTrue</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">IfSeqFalse</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">WhileSeqTrue</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">WhileSeqFalse</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">SeqSeq</td><td style="background-color:#C0FFC0">0.38</td><td style="background-color:#E0E0E0">---</td></tr>
</table>
<h2><span style="color:#008000">Theory "dl.Semantics": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="1">Obligations</td><td text-rotation="90">Alt-Ergo 2.4.0</td><td text-rotation="90">Z3 4.8.6</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">deduction</td><td style="background-color:#C0FFC0">3.21</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">valid_Uskip</td><td style="background-color:#C0FFC0">0.11</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">validUT_lm</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">validUT_triple</td><td style="background-color:#C0FFC0">0.06</td><td style="background-color:#E0E0E0">---</td></tr>
</table>
<h2><span style="color:#008000">Theory "dl.Rules": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo 2.4.0</td><td text-rotation="90">Z3 4.8.6</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">if_rule</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">core_while_rule</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">induction_pr</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="7" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="1">core_while_rule.0</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">core_while_rule.1</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">core_while_rule.2</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">core_while_rule.3</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">core_while_rule.4</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">core_while_rule.5</td><td style="background-color:#C0FFC0">0.07</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">core_while_rule.6</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">seq_assign_rule</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">seq_while_rule</td><td style="background-color:#C0FFC0">2.58</td><td style="background-color:#E0E0E0">---</td></tr>
</table>
<h2><span style="color:#008000">Theory "dl.ReverseRules": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="1">Obligations</td><td text-rotation="90">Alt-Ergo 2.4.0</td><td text-rotation="90">CVC4 1.8</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">expressiveness</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.09</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">skip_rule_rev</td><td style="background-color:#C0FFC0">0.09</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">assign_rule_rev</td><td style="background-color:#C0FFC0">0.10</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">while_rule_revFsqb</td><td style="background-color:#C0FFC0">0.36</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">seq_assign_rule_rev</td><td style="background-color:#C0FFC0">0.21</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">seq_while_rule_rev_Fsqb</td><td style="background-color:#C0FFC0">1.32</td><td style="background-color:#E0E0E0">---</td></tr>
</table>
<h2><span style="color:#008000">Theory "dl.DLSoundnessCompleteness": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="4">Obligations</td><td text-rotation="90">Alt-Ergo 2.4.0</td><td text-rotation="90">CVC4 1.8</td><td text-rotation="90">Z3 4.8.6</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="4">VC for infUT_sound_complete</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="4">split_vc</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="34" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.05</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.05</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">split_vc</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="22" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="2">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">split_vc</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="9" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.10</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.06</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.05</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.10</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.07</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">split_vc</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="9" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">0.77</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.05</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.32</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.05</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">0.25</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.12</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.05</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.05</td></tr>
</table>