Now that we got out of the way this
initial set of basic definitions. Let's go back to our
main concept, which is software verification. We said that software
is buggy, and because software is buggy, we need to
verify the software as much as we can. But how
can we verify software? There are several ways to verify
a software system. Among those, we will discuss four mainstream
approaches. The first one is testing, also called dynamic verification.
The second approach is static verification. The third approach is
inspections. And finally, we're going to consider a fourth approach which is
formal proofs of correctness. So what I'm going to do
next, I'm going to first provide an overview of these approaches and
then discuss some of them in more depth and please
note that although we will discuss all four approaches we will
spend most of our time on software testing. As software
testing is the most popular and most used approach in industry.
So let's start with our overview and in particular
with testing. Testing a software system means exercising the system
to try to make it fail. More precisely, let's consider
a program. Its input domain, which is the set of
all the possible inputs for the program and, its output
domain, which is a set of all the possible corresponding
outputs. Given this context, we can define what a test
case is. A test case is a pair that consists
of a, an input from the input domain D,
and then, expected output O from the output domain.
And O is the element in the output domain
that a correct software would produce when ran against I.
We can also define the concept of test suite,
which is a set of test cases, and we're going to
use these two concepts of test case and test
suite quite a bit in the rest of the lessons.
Subject verification, tries to identify specific classes of problems
in the program. Such as null pointer dereferences. And
unlike testing, what it does is that it does
not just consider individual inputs, it instead considers all
possible inputs for the program. So it consider in
a sense all possible executions of the program and
all possible behaviors of the program, that's why we
save the verification unlike testing it's complete. The 3rd technique
we are going to consider is inspections,
and inspections are also called reviews or walkthroughs.
And unlike the previous techniques, inspections are a
human intensive activity, more precisely, they are a
manual and group activity in which several
people from the organization that developed the software,
look at the code or other artifacts developed
during the software production and try to identify
defects in these artifacts. And interestingly inspections
have been shown to be quite effective in
practice and that's the reason why they're used
quite widely in the industry. Finally, the last
technique I want to mention is Formal
Proof (of correctness). Given a software specification, and
actually a formal specification, so a document that
formally defines and specifies the behavior, the expected
behavior of the program. A form of proof of
correctness proves that the program being verified, actually implements
the program specification and it does that through a
sophisticated mathematical analysis of the specifications and of the code.