1 files changed, 195 insertions, 0 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
new file mode 100644
index 0000000..36a58ee
--- /dev/null
+++ b/usth/ICT2.7/P4L1 General Concepts Subtitles/11 - Pros and Cons of Approaches - lang_en_vs4.srt
@@ -0,0 +1,195 @@
+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.