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.