CollisionAvoidanceSystem/CASystem_unproven.html at master · varuna-v/CollisionAvoidanceSystem · GitHub

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
<!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\CASystem.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\CASystem.pd</h2>
<h3>Generated by Perfect Developer Free Edition at 10:14:15 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 1 of 1 verification conditions.</h3>
<br>
<br>
<a NAME="1"> </a><span class="obligationdesc">Failed to prove verification condition: </span>Precondition of 'changeCraftHeight' satisfied<br>
<span class="obligationdesc">Suggestion: </span>Add extra precondition: <span class="keyword">exists</span> c::<span class="keyword">self</span>.atc.aircrafts &bull; c.identification = identification<br>
<span class="obligationdesc">In the context of class: </span>CASystem, declared at: C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\CASystem.pd (7,1)<br>
<span class="obligationdesc">Condition generated at: </span>C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\CASystem.pd (24,18)<br>
<span class="obligationdesc">Condition defined at: </span>C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\AirTrafficController.pd (65,13)<br>
<span class="obligationdesc">To prove: </span><span class="keyword">exists</span> c::<span class="keyword">self</span>.atc.aircrafts &bull; c.identification = identification<br>
<span class="obligationdesc">Reason: </span>Exhausted rules<br>
<ul>
<li><span class="obligationdesc">Could not prove:</span><br>
?a.identification = identification<br>
<span class="obligationdesc">Where:</span><br>
?a<span class="obligationdesc"> can be given any value of type </span>Aircraft<span class="obligationdesc"> satisfying: </span>?a <span class="keyword">in</span> <span class="keyword">self</span>.atc.aircrafts<br>
<li><span class="obligationdesc">Could not prove any of:</span><br>
#?a.identification &le; <span class="literal">0</span><br>
$b_i<sub>?a</sub>(?a) &lt; <span class="literal">0</span><br>
#?a.identification &le; $b_i<sub>?a</sub>(?a)<br>
<span class="obligationdesc">Where:</span><br>
?a<span class="obligationdesc"> can be given any value of type </span>Aircraft<span class="obligationdesc"> satisfying: </span>?a <span class="keyword">in</span> <span class="keyword">self</span>.atc.aircrafts<br>
</ul>
<br>
<br>
<h3>End of unproven verification conditions for file C:\Users\User\Desktop\Third Year Project\CollisionAvoidanceSystem\CASystem.pd</h3>
</body>
</html>