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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
|
1
00:00:00,230 --> 00:00:02,870
The four different techniques that we just discussed have
2
00:00:02,870 --> 00:00:06,120
a number of pros and cons. So next we
3
00:00:06,120 --> 00:00:08,780
are going to discuss the main pros and cons
4
00:00:08,780 --> 00:00:11,140
for these techniques, so as to be able to compare
5
00:00:11,140 --> 00:00:14,330
them. When testing is concerned the main positive about
6
00:00:14,330 --> 00:00:17,600
this technique is that it does not generate false
7
00:00:17,600 --> 00:00:21,740
alarms. In other words, it doesn't generate false positives.
8
00:00:21,740 --> 00:00:25,180
What that means, is that when testing generates a failure,
9
00:00:25,180 --> 00:00:27,230
that means that there is an actual problem in the
10
00:00:27,230 --> 00:00:30,060
code. The main limitation of testing, however, is that it
11
00:00:30,060 --> 00:00:33,680
is highly incomplete. Consider again the picture that we drew
12
00:00:33,680 --> 00:00:36,430
a little earlier. The one representing the input domain of
13
00:00:36,430 --> 00:00:39,430
the program being tested. Even in the best scenario, testing
14
00:00:39,430 --> 00:00:44,050
can consider only a tiny fraction of the problem domain,
15
00:00:44,050 --> 00:00:47,430
and therefor a tiny fraction of the program's behavior, and
16
00:00:47,430 --> 00:00:50,308
we'll say a lot more about that in the following lessons.
17
00:00:50,308 --> 00:00:53,780
Static verification, unlike testing, has the main advantage
18
00:00:53,780 --> 00:00:57,320
that it considers all program behaviors. If we
19
00:00:57,320 --> 00:01:00,370
look back at our diagram, whereas testing will
20
00:01:00,370 --> 00:01:04,010
select only a few of those inputs, static verification
21
00:01:04,010 --> 00:01:07,120
will consider them all. Unfortunately, however, this comes
22
00:01:07,120 --> 00:01:08,990
with a price. Due to limitation of this
23
00:01:08,990 --> 00:01:11,490
kind of analysis and due to infeasibility issues,
24
00:01:11,490 --> 00:01:15,260
static verifiation considers not only all the possible behaviours,
25
00:01:15,260 --> 00:01:18,870
but also some impossible behaviors. And what that means is
26
00:01:18,870 --> 00:01:22,472
that static gratificaition can generate false positives. And this is,
27
00:01:22,472 --> 00:01:24,590
in fact, the main issue with static verification techniques. As
28
00:01:24,590 --> 00:01:28,550
we will further discuss later in the class, static verification can
29
00:01:28,550 --> 00:01:31,280
generate results that are not true. For example, it might
30
00:01:31,280 --> 00:01:33,970
report a possible no point of the refernce that cannot
31
00:01:33,970 --> 00:01:37,590
actually occur in practice. The strongest point about inspections is
32
00:01:37,590 --> 00:01:40,950
that, when they're done in a rigorous way, they're systematic and
33
00:01:40,950 --> 00:01:43,420
they result in a thorough analysis of the code.
34
00:01:43,420 --> 00:01:46,840
They are nevertheless a manual process, a human process.
35
00:01:46,840 --> 00:01:49,890
So they're not formal and their effectiveness may depend
36
00:01:49,890 --> 00:01:53,560
on the specific people performing the inspection. So its results
37
00:01:53,560 --> 00:01:57,150
can be subjective. Finally, the main pro about formal
38
00:01:57,150 --> 00:02:01,090
proofs of correctness is that they provide strong guarantees.
39
00:02:01,090 --> 00:02:03,740
They can guarantee that the program is correct, which
40
00:02:03,740 --> 00:02:06,280
is not something that any of the other approaches can
41
00:02:06,280 --> 00:02:09,505
do, including study verification. But the main limitation of
42
00:02:09,505 --> 00:02:12,680
formal proofs is that they need a form of specification,
43
00:02:12,680 --> 00:02:15,750
a complete mathematical description of the expected behavior of
44
00:02:15,750 --> 00:02:19,060
the whole program, and unfortunately such a specification is rarely
45
00:02:19,060 --> 00:02:21,920
available, and it is very complex to build one.
46
00:02:21,920 --> 00:02:25,170
In addition, it is also very complex, and possibly expensive,
47
00:02:25,170 --> 00:02:27,720
to prove that the program corresponds to a specification.
48
00:02:27,720 --> 00:02:30,990
That is a process that requires strong mathematical skills and,
49
00:02:30,990 --> 00:02:32,551
therefore, a very specialized personnel.
|
