-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathVector_unproven.html
More file actions
61 lines (61 loc) · 7.26 KB
/
Vector_unproven.html
File metadata and controls
61 lines (61 loc) · 7.26 KB
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
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<title>Unproven verification conditions for file C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\Vector.pd</title>
<style type="text/css">
body { line-height: 1.4em }
sub { font-size: 75%; font-family: Arial, Helvetica, sans-serif; vertical-align: -0.6ex; line-height: 0 }
.keyword { font-weight: bold }
.highlight { color: #0000FF; font-weight: bold }
.literal { color: #008800 }
.proofcomment { color: #DD0000; font-style: italic }
.obligationdesc { color: #0000AA }
</style>
</head>
<body>
<h2>Unproven verification conditions for file C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\Vector.pd</h2>
<h3>Generated by Perfect Developer Free Edition at 10:18:14 UTC on Monday March 23rd 2015</h3>
<h4>Escher Verification Studio file versions</h4>
EscherTool 6.10.01<br>
builtin 6.10.00.00<br>
rubric 6.10.00.00<br>
<h3>Failed to prove 2 of 12 verification conditions.</h3>
<br>
<br>
<a NAME="4"> </a><span class="obligationdesc">Failed to prove verification condition: </span>Precondition of 'operator ^' satisfied<br>
<span class="obligationdesc">Suggestion: </span>Add extra precondition: <span class="literal">0.0</span> ≤ ((<span class="literal">-2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">-2.0</span> * <span class="keyword">self</span>.y * other.y) + (<span class="literal">-2.0</span> * <span class="keyword">self</span>.z * other.z) + (<span class="keyword">self</span>.x ^ <span class="literal">2</span>) + (other.x ^ <span class="literal">2</span>) + (<span class="keyword">self</span>.y ^ <span class="literal">2</span>) + (other.y ^ <span class="literal">2</span>) + (<span class="keyword">self</span>.z ^ <span class="literal">2</span>) + (other.z ^ <span class="literal">2</span>))<br>
<span class="obligationdesc">In the context of class: </span>Vector, declared at: C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\Vector.pd (7,1)<br>
<span class="obligationdesc">Condition generated at: </span>C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\Vector.pd (35,66)<br>
<span class="obligationdesc">Condition defined at: </span>built in declaration<br>
<span class="obligationdesc">To prove: </span><span class="literal">0.0</span> ≤ ((((<span class="keyword">self</span>.x - other.x) ^ <span class="literal">2</span>) + ((<span class="keyword">self</span>.y - other.y) ^ <span class="literal">2</span>)) + ((<span class="keyword">self</span>.z - other.z) ^ <span class="literal">2</span>))<br>
<span class="obligationdesc">Reason: </span>Prover made no progress within the boredom limit<br>
<ul>
<li><span class="obligationdesc">Could not prove any of:</span><br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.z * other.z)) ≤ (other.z ^ <span class="literal">2</span>)<br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.z * other.z)) ≤ (<span class="keyword">self</span>.z ^ <span class="literal">2</span>)<br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.z * other.z)) ≤ ((<span class="keyword">self</span>.z ^ <span class="literal">2</span>) + (other.z ^ <span class="literal">2</span>))<br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.z * other.z)) ≤ ((other.y ^ <span class="literal">2</span>) + (other.z ^ <span class="literal">2</span>))<br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.z * other.z)) ≤ ((other.y ^ <span class="literal">2</span>) + (<span class="keyword">self</span>.z ^ <span class="literal">2</span>))<br>
</ul>
<br>
<br>
<a NAME="7"> </a><span class="obligationdesc">Failed to prove verification condition: </span>Precondition of 'operator ^' satisfied<br>
<span class="obligationdesc">Suggestion: </span>Add extra precondition: (~(<span class="keyword">self</span>.x = other.x) | ~(<span class="keyword">self</span>.y = other.y)) ==> (<span class="literal">0.0</span> ≤ ((<span class="literal">-2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">-2.0</span> * <span class="keyword">self</span>.y * other.y) + (<span class="keyword">self</span>.x ^ <span class="literal">2</span>) + (other.x ^ <span class="literal">2</span>) + (<span class="keyword">self</span>.y ^ <span class="literal">2</span>) + (other.y ^ <span class="literal">2</span>)))<br>
<span class="obligationdesc">In the context of class: </span>Vector, declared at: C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\Vector.pd (7,1)<br>
<span class="obligationdesc">Condition generated at: </span>C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\Vector.pd (31,53)<br>
<span class="obligationdesc">Condition defined at: </span>built in declaration<br>
<span class="obligationdesc">To prove: </span><span class="literal">0.0</span> ≤ (((<span class="keyword">self</span>.x - other.x) ^ <span class="literal">2</span>) + ((<span class="keyword">self</span>.y - other.y) ^ <span class="literal">2</span>))<br>
<span class="obligationdesc">Reason: </span>Exhausted rules<br>
<ul>
<li><span class="obligationdesc">Could not prove any of:</span><br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y)) ≤ <span class="literal">0.0</span><br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y)) ≤ (other.y ^ <span class="literal">2</span>)<br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y)) ≤ (<span class="keyword">self</span>.y ^ <span class="literal">2</span>)<br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y)) ≤ (other.x ^ <span class="literal">2</span>)<br>
((<span class="literal">2.0</span> * <span class="keyword">self</span>.x * other.x) + (<span class="literal">2.0</span> * <span class="keyword">self</span>.y * other.y)) ≤ (<span class="keyword">self</span>.x ^ <span class="literal">2</span>)<br>
</ul>
<br>
<br>
<h3>End of unproven verification conditions for file C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\Vector.pd</h3>
</body>
</html>