In this paper we propose a method for inferring invariants for loops in Java programs. An example of a simple while loop is used throughout the paper to explain our approach. The method is based on a combination of symbolic execution and computing fixed points via predicate abstraction. It reuses the axiomatisation of the Java semantics of the KeY system. The method has been implemented within the KeY system which allows to infer invariants and perform verification within the same environment. We present in detail the results of a non-trivial example.
A notorious difficulty in the formal verification of programs is the treatment of loop constructs. An array of techniques has been developed to address this problem. Among these techniques the use of loop invariants is particularly attractive since it does not compromise on the rigour of verification and runs completely automatically, once the correct invariants are provided. In this paper we will try to answer the question how to find invariants.
Several techniques for automatically inferring invariants of a program exist.
One general approach is dynamic analysis, i.e., analysing the program by
executing it with concrete input values. A tool implementing dynamic invariant
inference is Daikon [
Stronger guarantees can be provided by static analysis, i.e., analysing the
program by examining its source code without actually executing it on concrete
inputs. A common paradigm in static analysis, which is also used in program
verification, is symbolic execution [
Predicate abstraction [
In the invariant inference method described in [
The organisation of this paper is as follows: in Sect. 2, we review our program logic for Java Card and its axiomatisation of the programming language semantics. In Sect. 3, we introduce a simple example for a program and its invariants. Using this example, we then explain our approach for inferring invariants in Sect. 4. The implementation of the approach within the KeY system is sketched in Sect. 5, and the results of initial experiments with the implementation are documented in Sect. 6. Finally, we conclude in Sect. 7.
Our approach is based on the program logic Java Card DL [3, Chapt. 3], which
is a version of dynamic logic [
Formulas of the form ϕ → [p]ψ are similar to Hoare triples {ϕ}p{ψ}: they express that if p terminates after being started in a state which satisfies ϕ, then the resulting state satisfies ψ. For example, the meaning of the formula . . o.f = 27 → [o.f++;]o.f = 28 is: if the current value of the field f of the object pointed to by the program variable o is 27, then after executing the statement o.f++; the value of the field has changed to 28. This formula is valid, i.e., it holds in all possible states.
Proofs of the validity of Java Card DL formulas can be performed by means of a sequent calculus. A sequent is a construct Γ ` Δ, where Γ and Δ are sets of formulas. Its semantics is the same as that of the formula V Γ → W Δ, and in the following we do not strictly distinguish between sequents and their equivalent formulas. An example for a sequent calculus rule is andRight: Γ ` ϕ, Δ Γ ` ϕ0, Δ Γ ` ϕ ∧ ϕ0, Δ andRight The (schematic) sequents Γ ` ϕ, Δ and Γ ` ϕ0, Δ are the premisses of the rule, and the sequent Γ ` ϕ ∧ ϕ0, Δ is the conclusion of the rule. A rule is sound if validity of its premisses implies validity of its conclusion. A proof for a sequent is constructed by applying rules from bottom to top; if all leaves of the resulting tree are valid, then the root sequent must be valid as well. The particular rule andRight deals with a conjunction on the right side of the sequent arrow by splitting the proof tree into two branches.
Formulas with modal operators are handled by rules which perform a symbolic execution of the Java Card program within the modality. These rules operate on the active statement of the program, i.e., the first basic statement following a non-active prefix of opening braces, beginnings of try blocks and the like. This prefix is denoted by π, and the rest of the program behind the active statement by ω. For example, the active statement of the following program is i = 0: { try { i = 0; i++; } catch(Exception e) { i = 27; } } | {πz } | {ωz }
The Java Card DL calculus, as it is implemented in the KeY system, currently contains approximately 1700 rules, of which about 1300 formalise the semantics of Java Card. As we cannot describe all of them here, we restrict our presentation to representative rules for the three basic programming constructs in imperative languages: assignments, conditional statements, and loops. We begin with assignments, which can be symbolically executed with Γ 0, x =. e0 ` [π ω]ψ, Δ0 Γ ` [π x = e; ω]ψ, Δ assignment where the expression e must not have side effects, and where Γ 0, e0 and Δ0 result from Γ , e and Δ, respectively, by substituting a fresh program variable x0 for x. This rule replaces the assumptions about the initial state of the program by their strongest postcondition under the assignment statement. For example, it transforms the sequent i = 27 ` [i=i+1;]i = 28 into i0 =. 27, i =. i0 + 1 ` i = 28.
. . .
As formulated here, the assignment rule only works for assignments to local
program variables. Assignments to fields or array slots are more complex
because of aliasing, i.e., the phenomenon that the same memory location may be
referred to by different names. They can nevertheless be handled along the same
lines as assignments to local variables, but this leads to somewhat complicated
formulas containing case distinctions for the possible aliasing situations. For
example, symbolically executing o1.f =. 27 ` [o2.f = 0; ]o1.f =. 27 in this way
yields o1.f 0 =. 27, ∀x.(x.f =. if (x =. o2)then(0)else(x.f 0)) ` o1.f =. 27. The
KeY system normally avoids these complications as far as possible by treating
assignments in a different way, which is based on a concept called updates [
Conditional statements can be handled with this rule: Γ ` (e =. true → [π p ω]ψ) ∧ (¬e =. true → [π q ω]ψ), Δ ifElse Γ ` [π if(e) p else q ω]ψ, Δ Again, the occurring Java Card expression must not have side effects. This restriction is never severe, because a program can always be transformed such that an expression is separated from its side effects; the Java Card DL calculus contains rules which perform such transformations. The ifElse rule symbolically executes a conditional statement by creating two conjuncts which describe the case that the guard expression is true and the case that it is false, respectively. Typically, the next step is to split the proof tree by applying the andRight rule.
Loops can be symbolically executed with the loopUnwind rule Γ ` [π if(e){p while(e) p} ω]ψ, Δ Γ ` [π while(e) p ω]ψ, Δ
loopUnwind where, as usual, the expression e must not have side effects. This is a simplified version of the actual rule which is sound only if the loop body does not contain break or continue statements. It transforms the loop into a conditional statement: if the guard expression is satisfied, then the loop body is executed once before getting to the loop again; otherwise, the loop is not entered. Since its premiss again contains the loop, the unwind rule on its own only works for loops which terminate after a statically known and sufficiently small number of iterations. In the general case, loops cannot be handled by symbolic execution alone. Instead, an invariant rule can be used, i.e., a rule which makes use of a loop invariant. This loop invariant normally has to be provided manually from the outside. 3
As a simple example for a program and its invariants, we will use the following piece of Java Card code, which computes the maximal positive element of an integer array a: max = 0; i = 0; while(i < a.length) { if(a[i] > max) max = a[i]; i++; }
The program is visualised as a control flow graph in Fig. 1. The nodes of
this graph represent the basic commands and guard expressions of the program,
and the edges stand for flow of control between the nodes. Control enters the
program through the node marked entry, and leaves it through the node marked
exit (for the sake of readability, we ignore here that the program terminates
abruptly if a =. null holds). The control flow graph is annotated with exemplary
invariants at interesting program points. Note that in this paper we are talking
about invariants in the classical sense, i.e., first-order formulas which always
hold when control flow reaches a specific program point such as a loop entry.
The notion of “class” or “object” invariants for object-oriented programs [
Our example invariants for the program are as follows: at the entry node, we assume nothing about the program state, so the invariant here is true. After . the first assignment statement, max = 0 always holds–this is the strongest postcondition of true under the assignment statement. Next is the loop invariant: every time control flow reaches the loop entry, ∀x.(0 ≤ x < i → a[x] ≤ max) is satisfied. Unlike the loop invariant, the remaining invariants can again easily be derived from their predecessors as strongest postconditions. In particular, the entry max=0; i=0; i<a.length true false a[i]>max true false
exit max=a[i]; i++; true max ≐ 0 8 x:(0 · x <i ! a[x] · max) 8 x:(0 · x < i ! a[x] · max) ^ i < a.length 8 x:(0 · x <i ! a[x] · max) ^ i ¸ a.length 8 x:(0 · x < i ! a[x] · max) ^ i < a.length
^ a[i] > max 8 x:(0 · x · i ! a[x] · max) ^ i < a.length invariant attached to the exit node, i.e., the postcondition of the program as a whole, immediately follows from the loop invariant and the negation of the loop guard expression. 4
Our approach is embedded in the overall process of program verification which we imagine has reached a state where a typical goal ϕ → [p]ψ has to be proved. The basic idea is to extend the usual symbolic execution of p in the Java Card DL calculus by fixed-point iteration and predicate abstraction, and thereby turn the proving process into a form of abstract interpretation. To help the reader understand how this works out exactly, we outline our approach with the particular instantiations of ϕ, p and ψ given in Fig. 2(1): the goal is to prove that after executing the program introduced in Sect. 3, all elements of the array are less than or equal to max. Symbolic execution of the program begins with applying the assignment rule to the first two assignments, which leads to the new proof obligation shown in Fig. 2(2). The effect of the two assignments manifests itself . . in the two additional assumptions max = 0 and i = 0. Now, the active statement of the program is the while loop.
The guiding principle of our construction is to always view the formula on the left hand side of the implication as a candidate for an invariant at the program point reached before the active statement of the program occurring in the modality on the right hand side of the implication. According to this principle, the formula ϕ1 in Fig. 2(2) is a first candidate for the loop invariant.
The next step in the symbolic execution has to deal with two cases: the loop is not entered and the loop is unfolded at least once. Technically, we apply the loopUnwind rule followed by the ifElse rule, and obtain the conjunction of the two implications shown in Fig. 2(3).
We refrain from splitting the proof by applying the andRight rule, and for the moment concentrate on the first conjunct. The active statement of its box modality on the right hand side is a conditional statement. Thus, the next symbolic execution step is to apply the ifElse rule, which produces two conjuncts in place of one. Again, we do not split this conjunction with the andRight rule. Instead, the assignment max = a[i]; in the body of the conditional statement is executed, yielding the proof goal shown in Fig. 2(4). Notice that for the first time the assignment rule necessitates the introduction of a new program variable max 0 to hold the previous value of max.
There is a fundamental difference between the first two conjuncts in Fig. 2(4) and the third: the first two refer to the same point in program execution. More precisely, the right hand sides of the first two implications coincide, so we can apply the merge rule
Γ ` (ϕ ∨ ϕ0) → ψ, Δ Γ ` (ϕ → ψ) ∧ (ϕ0 → ψ), Δ merge which replaces the first two implications by one, logically equivalent, implication, Fig. 3(5). This one implication describes the combined effects of the two execution paths, just like in the control flow graph (Fig. 1) there is only one node for the assignment i++;, even though it can be reached via several paths. Making such merging steps possible is the reason why we did not and will not apply the andRight rule to split the proof.
After symbolic execution of i++;, the last statement of the loop body, we reach in Fig. 3(6) the same program point again that we had already considered in Fig. 2(2), namely the loop entry. Now, we have two invariant candidates ϕ1 from (2) and ϕ2 from (6) for the same program point. Naturally, we consider their disjunction ϕ1 ∨ ϕ2 as our new invariant candidate, which is shown in Fig. 3(7). Technically this is achieved by applying the loopMerge rule Γ ` (ϕ ∨ ϕ0) → [π while(e) p ω]ψ, Δ Γ ` (ϕ → [π while(e) p ω]ψ) ∧ (ϕ0 ∧ ¬e =. true → [π ω]ψ), Δ loopMerge true → [{ max = 0; i = 0; while(i < a.length) { if(a[i] > max) max = a[i]; i++; } }] ∀x.(0 ≤ x < a.length → a[x] ≤ max)
| {ψz0 } . . max = 0 ∧ i = 0 → [{ while(i < a.length) { | {ϕz1 } if(a[i] > max) max = a[i];
i++;
Fig. 2. Invariant inference for the example program (first part). (1) (2) (3) (4) (max 0 =. 0 ∧ i = 0 ∧ i < a.length ∧ a[i] > max 0 ∧ max = a[i]
. .
. . ∨ max = 0 ∧ i = 0 ∧ i < a.length ∧ a[i] ≤ max) → [{ i++; while(i < a.length) { if(a[i] > max) max = a[i]; i++;
Fig. 3. Invariant inference for the example program (second part). (5) (6) (7) (8) (9) where e must not have side effects. The same principle guides both the merge and the loopMerge rule: the effects of several execution paths are combined in one implication.
If ϕ1 was logically equivalent to ϕ1 ∨ ϕ2, we could stop here and declare ϕ1
to be our prime candidate for the loop invariant: it would be a fixed point of
our iterative inference process. But as you can easily see, this is not the case in
our example. So, we have to go on, unfold the loop body once more, obtain a
loop invariant candidate ϕ3 after the second iteration, check whether ϕ1 ∨ ϕ2
is logically equivalent to ϕ1 ∨ ϕ2 ∨ ϕ3, and then stop or go on accordingly. The
problem with this plan of action is that it might (and, in the example, would)
not terminate. This is where predicate abstraction as it is, e.g., described in [
.
P = {i = 0, 0 ≤ i, i ≤ 1, ∀x.(0 ≤ x < i → a[x] ≤ max)} .
| {pz1 } | {pz2 } | {pz3 } | {pz4 }
In general P might be chosen by following heuristics, e.g., include all parts of
the invariant candidate accumulated before the first unfolding of the loop, the
loop guard, and parts of the postcondition ψ. In addition one might include in P
all the usual suspect invariants, as is, e.g., done in [
After symbolically executing the loop body for the second time and again applying loopMerge and abstraction, we arrive at p2 ∧ p4. Since P is of finite size, this process of eliminating predicates must eventually terminate. In the example, it does so after just one more iteration: if we symbolically execute the loop body a third time, the new invariant candidate reached after applying loopMerge and abstraction is again p2 ∧ p4. We have reached a fixed point and stop iterating the while loop. Technically speaking, instead of applying the loopUnwind rule we apply Γ ` ϕ ∧ ¬e =. true → [π ω]ψ, Δ loopEnd Γ ` ϕ → [π while(e)p ω]ψ, Δ where e must not have side effects. In our running example this rule application results in Fig. 3(9).
There is one problem with the loopEnd rule: Unlike the other rules introduced in this section, it is not sound, as you can easily see. Applying it is sound if the formula ϕ is an invariant for the loop. In situations like the one in the example, we have good reason to believe that this is the case: ϕ is a fixed point of accumulated symbolic executions of the loop body, so it should hold at the loop entry in all possible concrete executions. This is however not quite guaranteed; for example, non-symbolic-execution rules might have been applied in between, disrupting the inference process. Formally prohibiting the application of the loopEnd rule in such situations is conceivable, but complicated. In our context, this is not a necessity: Our implementation prevents unsound applications in a heuristic manner, and if in very rare cases these heuristics should fail and an inferred “invariant” not really be an invariant, this error would be caught when trying to use the false invariant for a regular proof with the invariant rule.
What is a good loop invariant? After all the logical constant true is always an invariant. In our scenario where invariant inference is just one part of an overall program verification effort the answer is easy: a loop invariant is good if it allows to successfully complete the overall proof goal. This is the case in our example, since Fig. 3(9) can easily be seen to be universally valid.
In summary, our approach is as follows. The analysed program is symbolically executed with the program rules of the Java Card DL calculus, but without intertwining this process with applications of other rules such as andRight. The symbolic execution is coordinated such that it follows the structure of the control flow graph; in particular, at confluences in the graph, the conjuncts describing the predecessors are combined using the merge and loopMerge rules. Each application of loopMerge is followed by an application of the abstraction rule. After applying abstraction, it is checked whether the resulting abstracted loop invariant candidate is a fixed point, i.e., whether the previous such candidate consisted of the same predicates. If so, it is taken as the inferred loop invariant, and loopEnd is applied. Otherwise, the loop is symbolically executed once again. This process works completely automatically, except that the user may choose to help it find better invariants by specifying predicates for each loop once in the beginning. 5
We have implemented our method as an extension of the KeY system. The core
element of this implementation are the rules introduced in Sect. 4. The bottleneck
of the approach clearly lies in the abstraction rule: it requires checking for each
predicate p ∈ P whether p is implied by the invariant candidate. These checks
are implemented as calls to an external automated first-order theorem prover
such as Simplify [
Besides the rules themselves, the implementation also comprises a heuristic predicate generator, which automatically creates many of the “usual suspect” invariant elements, such as ordering comparisons between integer program variables, or equality and inequality between variables of a reference type. The predicate generator is complemented by the possibility to manually enter predicates. No quantified formulas are generated automatically, as the number of predicates would get too large to be manageable. However, manually entered predicates are allowed to contain free variables; such predicates are then universally closed by the predicate generator, using various guards. For example, if the user specifies the predicate a[x] ≤ max, the predicate generator adds ∀x.(0 ≤ x < i → a[x] ≤ max), together with many other similar predicates.
The final element of the implementation is a proof search strategy, which controls the automatic application of the rules as it is necessary for invariant inference. In particular, the strategy prohibits the application of non-symbolicexecution rules, and it coordinates symbolic execution of several modalities such that it follows the control flow graph: if, e.g., the current proof goal is (ϕ1 → [max = a[i]; i++;]ψ) ∧ (ϕ2 → [i++;]ψ), symbolic execution of the second conjunct is stopped until max = a[i]; has been symbolically executed in the first conjunct and the merge rule can be applied. 6
We tested our implementation on selection sort, a well-known and comparatively simple sorting algorithm with quadratic time complexity. The basic idea of the algorithm is to find the smallest element of the array to be sorted, swap it with the first element, and iteratively repeat this process on the subarray starting at the second position. The exact proof obligation supplied to the KeY system is shown in Fig. 4. It states that, after invoking the program contained in the box modality on an integer array a which is not null and which has a positive length, the array is sorted. This specification is not strong enough to ensure that the program actually sorts the array; for example, a program could satisfy it by simply setting all array elements to zero. It is however sufficient for our purposes. The program itself is a straightforward Java Card rendering of selection sort. The temporary boolean variables condOuter and condInner are used to buffer the values of the loop guard expressions, which is necessary because our implementation of the invariant inference currently requires that the guard expressions must be simple program variables.
We manually entered the predicates (condOuter =. true ↔ i < a.length), (condInner =. true ↔ j < a.length), (a[x] ≤ a[y]), and (a[minIndex] ≤ a[x]), where x and y are free variables. The first two of these are necessary only because of the introduction of condInner and condOuter, and their generation could easily be automated. The other two require more ingenuity, but are still significantly easier to guess than the loop invariants themselves. Together with the automatically generated predicates, this lead to 8794 predicates for the inner loop and 16950 predicates for the outer loop.
Using Simplify as the external first-order theorem prover, the invariant inference process terminated after 3 iterations for the outer loop, containing 4, 4 and 2 iterations for the inner loop, respectively. 652 rules were applied in total. The overall running time on a 1.5 GHz Pentium M machine was about 8.5 minutes. Approximately 65% of this time was spent running Simplify, which was called exactly 800 times. The resulting loop invariants for the inner and the outer loop are shown in Fig. 5 and Fig. 6.
In addition to loop invariants, the invariant rule of the Java Card DL
calculus [
. ∧ a 6= null ∧ condOuter =. true
. ∧ (condOuter = true ↔ i < a.length)
. ∧ (condInner = true ↔ j < a.length)
Fig.6. Inferred invariant for the outer loop of selection sort. code), and, crucially, the loop invariants from Fig. 5 and Fig. 6, the KeY system (in normal mode) was able to automatically prove the validity of the formula from Fig. 4 in about 2 minutes. 7
We have presented a method for inferring invariants for while loops in Java programs that can seamlessly be integrated in program verification based on the symbolic execution paradigm. To do so this paradigm had to be adapted in two aspects. First, when using symbolic execution for program verification, intermediate proof goals that involve a case distinction are split into subgoals that are then proved separately. For invariant inference we have to avoid this splitting. Second, the ideas of fixed-point iteration and approximation are not present in the symbolic execution paradigm for program verification. So, we had to introduce them.
The approach has been implemented as an addition to the KeY verification system. The results of first experiments are very encouraging. But, since the success to a great deal depends on the heuristic choice of the set P of abstraction predicates, much more experience is needed to arrive at a dependable evaluation.
Approximation in static analysis typically takes the form of “erring on the safe side”, i.e., precision may be lost, but not correctness. In principle, our invariant inference is no exception: the inferred invariants may sometimes not be useful, but they should always indeed be invariants. However, since we introduced a rule which is not strictly sound, this is not guaranteed with the same high degree of confidence that is carried by the axioms from the KeY calculus. Remedying this imperfectness is one direction for future work. Nevertheless, the success rate of suggesting true invariants is already a lot higher than in dynamic analysis methods such as Daikon.
Another line of future work, which is more speculative, concerns the
generation of the abstraction predicates. One could investigate the use of CEGAR
(counterexample-guided abstraction refinement) techniques [