-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathupd-simpl.html
50 lines (49 loc) · 9.08 KB
/
upd-simpl.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
<h1>Why3 Proof Results for Project "upd-simpl"</h1>
<h2><span style="color:#008000">Theory "upd-simpl.UpdateApplication": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="3">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="3">VC for eq</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">VC for indom_exec</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.11</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for concat</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="11" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">unreachable point</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.07</td><td style="background-color:#E0E0E0">---</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:#C0FFC0">0.03</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="3" 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.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.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">0.05</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for lookup</td><td style="background-color:#C0FFC0">0.23</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for applyE</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="17" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">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="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.10</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">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="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.02</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="4" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</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.02</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">0.04</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:#C0FFC0">0.04</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</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:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for applyU</td><td style="background-color:#C0FFC0">0.29</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for applyB</td><td style="background-color:#C0FFC0">2.34</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for applyF</td><td style="background-color:#C0FFC0">3.36</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
</table>
<h2><span style="color:#008000">Theory "upd-simpl.Simplification": 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></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for simplE</td><td style="background-color:#C0FFC0">0.26</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for simplU</td><td style="background-color:#C0FFC0">0.53</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for simplB</td><td style="background-color:#C0FFC0">0.63</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for simplF</td><td style="background-color:#C0FFC0">2.14</td></tr>
</table>