Download Final report

…
client_check
instruction_1
instruction_2
…
Figure 3-9: Instructions after a client’s check.
A more complex analysis could check, for a call after instruction_1, whether the expressions
used for the precondition are not changed, but this would need an inter procedural dataflow
analysis.
3.3.
Specific Approach
Although the analysis described before is quite successful, the reward was not as great as
expected, since it turned out that it does not recognize the vast majority of the preconditions
(see experimental results), which is that an object must not be void. This is important
especially in object oriented programming, since it makes heavy use of references, and we
often have to make sure that an object is instantiated. Often a supplier offers a routine, where
the argument (or an attribute) must not be void, and he leaves it to the client, that he assures
this condition. In Eiffel this is declared in the precondition as well.
To illustrate the scenarios, where such precondition can be determined to be fulfilled, we give
a general sample to which we are going to confer in the special cases (Figure 1-1).
bar is
foo (a: A) is
require …
require
do
a /= Void
t /= Void
…
b := f (x)
do
foo (b)
…
…
end
ensure …
end
Figure 3-10: Sample, to show examples where a /= Void holds.
(1) In Eiffel, there are expanded types, which means, that instances of expanded types are
automatically initialized and cannot be void. Base types e.g. CHARACTER,
BOOLEAN, INTEGER, REAL and DOUBLE are also of expanded type. Now, if the
formal argument a is of expanded type, the precondition a /= Void holds.
(2) Same thing for the attribute t, if it is of expanded type.
(3) If b is a manifest constant it naturally cannot be void.
(4) If b is a call to a manifest constant.
(5) Same thing when b is Current. The self reference cannot be void.
28