diff options
Diffstat (limited to 'usth/ICT2.7/P4L1 General Concepts Subtitles/11 - Pros and Cons of Approaches - lang_en_vs4.srt')
| -rw-r--r-- | usth/ICT2.7/P4L1 General Concepts Subtitles/11 - Pros and Cons of Approaches - lang_en_vs4.srt | 195 |
1 files changed, 0 insertions, 195 deletions
diff --git a/usth/ICT2.7/P4L1 General Concepts Subtitles/11 - Pros and Cons of Approaches - lang_en_vs4.srt b/usth/ICT2.7/P4L1 General Concepts Subtitles/11 - Pros and Cons of Approaches - lang_en_vs4.srt deleted file mode 100644 index 36a58ee..0000000 --- a/usth/ICT2.7/P4L1 General Concepts Subtitles/11 - Pros and Cons of Approaches - lang_en_vs4.srt +++ /dev/null @@ -1,195 +0,0 @@ -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. |