-Now that we got out of the way this - -2
-initial set of basic definitions. Let's go back to our - -3
-main concept, which is software verification. We said that software - -4
-is buggy, and because software is buggy, we need to - -5
-verify the software as much as we can. But how - -6
-can we verify software? There are several ways to verify - -7
-a software system. Among those, we will discuss four mainstream - -8
-approaches. The first one is testing, also called dynamic verification. - -9
-The second approach is static verification. The third approach is - -10
-inspections. And finally, we're going to consider a fourth approach which is - -11
-formal proofs of correctness. So what I'm going to do - -12
-next, I'm going to first provide an overview of these approaches and - -13
-then discuss some of them in more depth and please - -14
-note that although we will discuss all four approaches we will - -15
-spend most of our time on software testing. As software - -16
-testing is the most popular and most used approach in industry. - -17
-So let's start with our overview and in particular - -18
-with testing. Testing a software system means exercising the system - -19
-to try to make it fail. More precisely, let's consider - -20
-a program. Its input domain, which is the set of - -21
-all the possible inputs for the program and, its output - -22
-domain, which is a set of all the possible corresponding - -23
-outputs. Given this context, we can define what a test - -24
-case is. A test case is a pair that consists - -25
-of a, an input from the input domain D, - -26
-and then, expected output O from the output domain. - -27
-And O is the element in the output domain - -28
-that a correct software would produce when ran against I. - -29
-We can also define the concept of test suite, - -30
-which is a set of test cases, and we're going to - -31
-use these two concepts of test case and test - -32
-suite quite a bit in the rest of the lessons. - -33
-Subject verification, tries to identify specific classes of problems - -34
-in the program. Such as null pointer dereferences. And - -35
-unlike testing, what it does is that it does - -36
-not just consider individual inputs, it instead considers all - -37
-possible inputs for the program. So it consider in - -38
-a sense all possible executions of the program and - -39
-all possible behaviors of the program, that's why we - -40
-save the verification unlike testing it's complete. The 3rd technique - -41
-we are going to consider is inspections, - -42
-and inspections are also called reviews or walkthroughs. - -43
-And unlike the previous techniques, inspections are a - -44
-human intensive activity, more precisely, they are a - -45
-manual and group activity in which several - -46
-people from the organization that developed the software, - -47
-look at the code or other artifacts developed - -48
-during the software production and try to identify - -49
-defects in these artifacts. And interestingly inspections - -50
-have been shown to be quite effective in - -51
-practice and that's the reason why they're used - -52
-quite widely in the industry. Finally, the last - -53
-technique I want to mention is Formal - -54
-Proof (of correctness). Given a software specification, and - -55
-actually a formal specification, so a document that - -56
-formally defines and specifies the behavior, the expected - -57
-behavior of the program. A form of proof of - -58
-correctness proves that the program being verified, actually implements - -59
-the program specification and it does that through a - -60
-sophisticated mathematical analysis of the specifications and of the code. -- cgit 1.4.1