1
00:00:00,320 --> 00:00:01,630
Now that we got out of the way this

2
00:00:01,630 --> 00:00:04,460
initial set of basic definitions. Let's go back to our

3
00:00:04,460 --> 00:00:08,770
main concept, which is software verification. We said that software

4
00:00:08,770 --> 00:00:11,730
is buggy, and because software is buggy, we need to

5
00:00:11,730 --> 00:00:14,690
verify the software as much as we can. But how

6
00:00:14,690 --> 00:00:17,960
can we verify software? There are several ways to verify

7
00:00:17,960 --> 00:00:21,150
a software system. Among those, we will discuss four mainstream

8
00:00:21,150 --> 00:00:25,410
approaches. The first one is testing, also called dynamic verification.

9
00:00:25,410 --> 00:00:29,400
The second approach is static verification. The third approach is

10
00:00:29,400 --> 00:00:33,000
inspections. And finally, we're going to consider a fourth approach which is

11
00:00:33,000 --> 00:00:36,090
formal proofs of correctness. So what I'm going to do

12
00:00:36,090 --> 00:00:39,570
next, I'm going to first provide an overview of these approaches and

13
00:00:39,570 --> 00:00:41,930
then discuss some of them in more depth and please

14
00:00:41,930 --> 00:00:44,430
note that although we will discuss all four approaches we will

15
00:00:44,430 --> 00:00:47,350
spend most of our time on software testing. As software

16
00:00:47,350 --> 00:00:50,850
testing is the most popular and most used approach in industry.

17
00:00:50,850 --> 00:00:53,050
So let's start with our overview and in particular

18
00:00:53,050 --> 00:00:58,050
with testing. Testing a software system means exercising the system

19
00:00:58,050 --> 00:01:01,680
to try to make it fail. More precisely, let's consider

20
00:01:01,680 --> 00:01:04,440
a program. Its input domain, which is the set of

21
00:01:04,440 --> 00:01:06,990
all the possible inputs for the program and, its output

22
00:01:06,990 --> 00:01:09,470
domain, which is a set of all the possible corresponding

23
00:01:09,470 --> 00:01:13,010
outputs. Given this context, we can define what a test

24
00:01:13,010 --> 00:01:16,360
case is. A test case is a pair that consists

25
00:01:16,360 --> 00:01:19,090
of a, an input from the input domain D,

26
00:01:19,090 --> 00:01:22,620
and then, expected output O from the output domain.

27
00:01:22,620 --> 00:01:25,950
And O is the element in the output domain

28
00:01:25,950 --> 00:01:29,670
that a correct software would produce when ran against I.

29
00:01:29,670 --> 00:01:32,170
We can also define the concept of test suite,

30
00:01:32,170 --> 00:01:34,840
which is a set of test cases, and we're going to

31
00:01:34,840 --> 00:01:37,730
use these two concepts of test case and test

32
00:01:37,730 --> 00:01:41,400
suite quite a bit in the rest of the lessons.

33
00:01:41,400 --> 00:01:44,980
Subject verification, tries to identify specific classes of problems

34
00:01:44,980 --> 00:01:47,620
in the program. Such as null pointer dereferences. And

35
00:01:47,620 --> 00:01:49,750
unlike testing, what it does is that it does

36
00:01:49,750 --> 00:01:53,610
not just consider individual inputs, it instead considers all

37
00:01:53,610 --> 00:01:56,594
possible inputs for the program. So it consider in

38
00:01:56,594 --> 00:01:59,366
a sense all possible executions of the program and

39
00:01:59,366 --> 00:02:02,402
all possible behaviors of the program, that's why we

40
00:02:02,402 --> 00:02:06,560
save the verification unlike testing it's complete. The 3rd technique

41
00:02:06,560 --> 00:02:08,755
we are going to consider is inspections,

42
00:02:08,755 --> 00:02:12,804
and inspections are also called reviews or walkthroughs.

43
00:02:12,804 --> 00:02:15,010
And unlike the previous techniques, inspections are a

44
00:02:15,010 --> 00:02:18,660
human intensive activity, more precisely, they are a

45
00:02:18,660 --> 00:02:22,520
manual and group activity in which several

46
00:02:22,520 --> 00:02:25,700
people from the organization that developed the software,

47
00:02:25,700 --> 00:02:29,190
look at the code or other artifacts developed

48
00:02:29,190 --> 00:02:31,888
during the software production and try to identify

49
00:02:31,888 --> 00:02:35,950
defects in these artifacts. And interestingly inspections

50
00:02:35,950 --> 00:02:37,580
have been shown to be quite effective in

51
00:02:37,580 --> 00:02:39,820
practice and that's the reason why they're used

52
00:02:39,820 --> 00:02:42,550
quite widely in the industry. Finally, the last

53
00:02:42,550 --> 00:02:45,100
technique I want to mention is Formal

54
00:02:45,100 --> 00:02:49,650
Proof (of correctness). Given a software specification, and

55
00:02:49,650 --> 00:02:53,370
actually a formal specification, so a document that

56
00:02:53,370 --> 00:02:57,410
formally defines and specifies the behavior, the expected

57
00:02:57,410 --> 00:03:00,320
behavior of the program. A form of proof of

58
00:03:00,320 --> 00:03:05,400
correctness proves that the program being verified, actually implements

59
00:03:05,400 --> 00:03:07,922
the program specification and it does that through a

60
00:03:07,922 --> 00:03:12,880
sophisticated mathematical analysis of the specifications and of the code.