The four different techniques that we just discussed have
a number of pros and cons. So next we
are going to discuss the main pros and cons
for these techniques, so as to be able to compare
them. When testing is concerned the main positive about
this technique is that it does not generate false
alarms. In other words, it doesn't generate false positives.
What that means, is that when testing generates a failure,
that means that there is an actual problem in the
code. The main limitation of testing, however, is that it
is highly incomplete. Consider again the picture that we drew
a little earlier. The one representing the input domain of
the program being tested. Even in the best scenario, testing
can consider only a tiny fraction of the problem domain,
and therefor a tiny fraction of the program's behavior, and
we'll say a lot more about that in the following lessons.
Static verification, unlike testing, has the main advantage
that it considers all program behaviors. If we
look back at our diagram, whereas testing will
select only a few of those inputs, static verification
will consider them all. Unfortunately, however, this comes
with a price. Due to limitation of this
kind of analysis and due to infeasibility issues,
static verifiation considers not only all the possible behaviours,
but also some impossible behaviors. And what that means is
that static gratificaition can generate false positives. And this is,
in fact, the main issue with static verification techniques. As
we will further discuss later in the class, static verification can
generate results that are not true. For example, it might
report a possible no point of the refernce that cannot
actually occur in practice. The strongest point about inspections is
that, when they're done in a rigorous way, they're systematic and
they result in a thorough analysis of the code.
They are nevertheless a manual process, a human process.
So they're not formal and their effectiveness may depend
on the specific people performing the inspection. So its results
can be subjective. Finally, the main pro about formal
proofs of correctness is that they provide strong guarantees.
They can guarantee that the program is correct, which
is not something that any of the other approaches can
do, including study verification. But the main limitation of
formal proofs is that they need a form of specification,
a complete mathematical description of the expected behavior of
the whole program, and unfortunately such a specification is rarely
available, and it is very complex to build one.
In addition, it is also very complex, and possibly expensive,
to prove that the program corresponds to a specification.
That is a process that requires strong mathematical skills and,
therefore, a very specialized personnel.