One of the most important challenges for SPARK users is to come up with adequate contracts and annotations, allowing GNATprove to verify the expected properties in a modular way. Among the annotations mandated by the SPARK toolset, the hardest to come up with are probably loop invariants.

As explained in a previous post, loop invariants are assertions that are used as cut point by the GNATprove tool to verify loop statements. In general, it is necessary to explicit in a loop invariant every information computed in the loop statement, or only the information computed in the last iteration will be available for proof.

A good loop invariant not only needs to describe how parts of variables modified by the loop evolve during the loop execution, but should also explicitly state the preservation of unmodified parts of modified variables. This last part is often forgotten, as it seems obvious to developers.

A previous post explains how GNATprove can automatically infer loop invariants for preservation of unmodified record components, and so, even if the record is itself nested inside a record or an array. Recently, this generation was improved to also support the simplest cases of partial array updates.

For a loop that updates an array variable (or an array component of a composite variable) by assigning to one (or more) of its indexes, GNATprove can infer preservation of unmodified fields in two cases:

• If an array is assigned at an index which is constant through the loop iterations, all the other components are preserved.
• If an array is assigned at the loop index, all the following components (or preceding components if the loop is reversed) are preserved.

This can be demonstrated on an example. Let us consider the following loop which swaps lines 5 and 7 of a square matrix of size 10:

We only describe in the invariant the effect of the computation on the modified part of M, that is, that it has effectively swapped the two lines up to index C. To discharge the following assertion, we also need to know that elements stored at other lines are preserved by the loop. As the first array index in the assignments is constant, GNATprove infers an invariant stating that components M (I, J) are not modified if I is not 5 or 7:

But it is not enough to verify our example. We also need to know that, at line 5 and 7, components stored after column C have not been modified yet, or we won't be able to verify the loop invariant itself. Luckily, as the second index of the assignments is the loop index, GNATprove can also infer this invariant, coming up with the additional:

The above example illustrates a case where GNATprove is able to successfully infer adequate loop invariants, leaving the user with only the most meaningful part to write. However, loop invariant generation for preservation of array components in GNATprove relies on heuristics, which makes it unable to deal with more complex cases. As an example, let us consider a slight variation of the above, which does not iterate directly on the column number, but introduces a shift of 1:

Like in the previous case, GNATprove can infer that lines different from 5 and 7 are preserved. Unfortunately, as the second index in the update is now a variable computation, it cannot come up with the second part of the invariant, and reports a failed attempt at verifying the loop invariant. The counter-example provided by GNATprove informs us that the verification could not succeed at the second line of the invariant (at line 5), for index I = 1, when updating column 2 (C = 1). Clearly, we are missing information about the preservation of components following column C at lines 5 and 7. If we add this invariant manually:

the proof is achieved again.

Another case for which GNATprove's heuristics are not precise yet, is relational updates. As an example, consider the following loop which increments the diagonal of a matrix:

Here again, we only specify the interesting part of the invariant, namely, that the elements encountered so far on the diagonal of the matrix have been incremented by one. Since we are updating the matrix exactly at the loop index, we could hope that GNATprove would be able to infer the appropriate invariant. Unfortunately, this is not the case, as the tool reports a failed attempt at verifying the assertion following the loop. Note that the loop invariant itself is proved, which means that GNATprove could infer that, at each iteration, the indexes following the current index had not been modified yet. So, what went wrong? The counter-example provided by GNATprove, here again, can be of some help. It precises that the verification was not completed when I is 8 and J is 9. Unsurprisingly, it means that the tool was not able to infer an invariant stating that elements outside the diagonal but located on columns smaller than the current index were preserved by the loop. Indeed, this would require handling specifically the case were both indexes of an update are the same value, which GNATprove does not do yet. If the following invariant is added manually to the loop, the verification succeeds: