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 [10]: to infer invariants for a program, Daikon first instruments it with state saving code at interesting program points. The instrumented program is then run through a user-specified test suite. Finally, the resulting data base of program states is analysed for properties which held in all of the test runs. These properties are somewhat likely to be invariants, but this is not guaranteed, because the test suite in general cannot cover all cases.
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 [16]: the analysed program is "executed", but with symbolic instead of concrete values for the program variables. Static invariant inference techniques are usually based on abstract interpretation [7]. Abstract interpretation can be understood as an approximative ("abstract") symbolic execution of the program, which deals with loops through fixed-point iteration.
Termination of this fixed-point iteration is ensured by the approximative nature of the used symbolic execution. An example of a tool which uses abstract interpretation for invariant inference is the static verifier Boogie [17].
Predicate abstraction [12] is a special variant of abstract interpretation, which has been used for invariant inference [11]. Here, the symbolic execution is itself not approximative, but as precise as possible (which corresponds to computing strongest postconditions). Instead, the necessary approximation is performed by explicit "abstraction" operations, which make use of an arbitrary, finite set of predicates over the variables of the program. The inferred invariants are constructed from these predicates. Thus, the problem of finding invariants is reduced to the simpler problem of guessing potentially useful predicates, which can be done heuristically or, when necessary, manually by the user.
In the invariant inference method described in [11], the semantics of the programming language is implicitly incorporated in the algorithms of the system. In our approach we start from the axiomatic semantics for Java Card developed within the KeY project. Java Card [15] is roughly a subset of Java which contains all object-oriented features but lacks concurrency, floating-point arithmetic, and dynamic class loading. The KeY system [1,3] is a deductive verification system for Java Card programs. It is based on an axiomatisation of the Java Card semantics within a program logic calculus, which follows the symbolic execution paradigm. The axiomatisation covers 100% of the Java Card language specification and a bit more with great precision. It has so far mainly been used for program verification, e.g., the Demoney case study, an electronic purse application provided by Trusted Logic S.A. [3,Chapt. 14], the verification of a Java Card implementation of the Schorr-Waite graph marking algorithm [3,Chapt. 15], and the verification of a part of a flight management system from Thales Avionics [14]. The most recent targets of verification with KeY have been an implementation of the Mondex banking card case study [23,22] and an implementation of the Java Card API [19]. The KeY symbolic execution rules for Java Card have lately also been used for model-based test generation [2,9]. In this paper we explore the possibility to use the KeY calculus and prover for inferring invariants, by incorporating fixed-point iteration and predicate abstraction. Besides the obvious benefit of reusing an existing formal semantics, this also has the advantage that the generation of loop invariants is an integrated part of the verification effort.
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 [13]. It extends first-order predicate logic by modal operators [p] ("box") and p ("diamond") for every legal sequence of Java Card statements p: the formula [p]ψ states that if execution of p terminates in a state s, then ψ holds in state s; the formula p ψ additionally requires that p does indeed terminate. In the following we only make use of the box modality [p]. The reason is that in this paper, we are interested in invariants, and invariants are not concerned with the issue of termination: they are safety properties, whereas termination is a liveness property.
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 Γ → ∆, and in the following we do not strictly distinguish between sequents and their equivalent formulas. An example for a sequent calculus rule is andRight:
The (schematic) sequents Γ ϕ, ∆ and Γ ϕ , ∆ are the premisses of the rule, and the sequent Γ ϕ ∧ ϕ , ∆ 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; } } ω 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
where the expression e must not have side effects, and where Γ , e and ∆ result from Γ , e and ∆, respectively, by substituting a fresh program variable x 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
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 . = 27, ∀x.(x.f . = if (x . = o2)then(0)else(x.f )) 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 [21]. However, for the purpose of inferring invariants, the classical way to handle assignments fits our needs better. The details of how this works out for complex assignments are given in [24]. In the following we restrict ourselves to the simple case of assignments to local variables, which amply suffices to explain our method.
Conditional statements can be handled with this rule:
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
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.
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:
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 [18] is related but lives at a different level of abstraction.
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 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.
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 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
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 (max
(max 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 [12], comes into play. To apply this method we first need to fix a set P of predicates.
For the example, we choose
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 [10]. As a final resort P could be customised by user interaction and trial and error. Once P is agreed upon we continue in the above example by replacing ϕ 1 ∨ ϕ 2 with its abstraction, which is the conjunction of all predicates p ∈ P for which (ϕ 1 ∨ ϕ 2 ) → p is a tautology. Formally, we apply the abstraction rule
where ϕ = {p ∈ P | ϕ → p is valid}. In our example we get ϕ = p 2 ∧ p 3 ∧ p 4 , see Fig. 3(8).
After symbolically executing the loop body for the second time and again applying loopMerge and abstraction, we arrive at p 2 ∧ p 4 . 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 p 2 ∧ p 4 . We have reached a fixed point and stop iterating the while loop. Technically speaking, instead of applying the loopUnwind rule we apply
where e must not have side effects. In our running example this rule application results in Fig. 3
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.
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 [8]. Decision procedures which support input in the SMT-LIB format [20] can also be used. Of course, such theorem prover calls are neither always successful nor computationally cheap. The lack of completeness is miti-gated by the fact that the predicates tend to be simple and thus manageable by the theorem prover. Acceptable performance can only be achieved by employing optimisations which reduce the number of necessary calls. Our implementation features several such optimisations. For example, it exploits implication relationships between predicates: if p 1 → p 2 is known to be valid, and the theorem prover has not been able to prove ϕ → p 2 , then there is no point in checking the validity of ϕ → p 1 . Possibly, performance could be improved further by using an existing predicate abstraction algorithm such as the one from [11] at this place.
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.
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 [4] makes use of modifier sets for loops, i.e., information about which memory locations may be modified by a loop. In the case of selection sort, appropriate modifier sets are {minIndex, j, condInner} for the inner loop, and {minIndex, j, condInner, temp, a[*], i, condOuter} for the outer loop. When supplied with these modifier sets (which are quite obvious from the program 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.
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 [6,5] to arrive at useful predicates in a less heuristic, more systematic manner.