From 8a7dfa0972c83fd811a4296e7373574bea4a28d0 Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Sun, 19 Jul 2020 20:34:40 +0700 Subject: [usth/ICT2.7] Remove Udacity transcribes --- .../10 - Verification Approaches - lang_en_vs4.srt | 239 --------------------- 1 file changed, 239 deletions(-) delete mode 100644 usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt (limited to 'usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt') diff --git a/usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt b/usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt deleted file mode 100644 index a671818..0000000 --- a/usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt +++ /dev/null @@ -1,239 +0,0 @@ -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. -- cgit 1.4.1