Download Final report

3.1.
Information Used for Verification
To perform the analysis within reasonable time, we limit the context of a considered call to
the following information:
(1) The caller routine (and the enclosing object), wherein the call is contained.
(2) The callees’ preconditions.
We are conscious, that the result is less rich than with an interprocedural or data flow
analysis. In return, the complexity of the analysis is considerably lower.
3.2.
General Approach
A client routine, which wants to make proper use of a called routine, has to make sure that he
fulfills the corresponding preconditions. Therefore, it has to somehow check this condition
before the target routine is eventually called, naturally with a control construct, if the
condition holds not for some other reason. As there are different possibilities to check such a
condition, the first task was to look for possible code patterns which can ensure a
precondition.
(1) Conditional
Because the conditional is an often used conditional instruction, it has been studied very
carefully for the possibility of assuring preconditions.
…
if condition then
call_a
…
else
call_b
…
end
…
Figure 3-2: Basic conditional construct, where condition is a boolean expression.
In the basic conditional construct as illustrated in Figure 3-2, there are already two
possibilities, where a client can possibly assure a call’s precondition.
a) condition implies call_a’s precondition
b) not condition implies call_b’s precondition
21