A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of string search, and to find a previously unknown bug in a faster version of string search called quick search. Frama-C and SPARK share similar history, techniques and goals. So it was tempting to redo the same proofs on equivalent code in SPARK, and completing them with a functional proof of the fixed version of quick search. This is what I'll present in this post.

Contrary to strings in C which start at index 0, standard strings in SPARK range over positive numbers, and usually start at index 1. I could have made my own strings to start at index 0, but there is no reason to stick to C convention when writing the algorithm in SPARK. At the same time, it's convenient to force the string to start at index 1 with an explicit predicate, which I do like that:

Following the order of exposure of Tommy M. McGuire's posts, here is the implementation for the brute force algorithm in SPARK:

I am doing here without the parameters n and h which were used in the C version to denote the length of strings needle and haystack, since these are readily available as attributes Haystack'Length and Needle'Length in SPARK. Since I'm working on strings starting at index 1, there are a few adjustments compared to the C version. The use of a temporary variable Diff is needed to detect that the inner loop was exited due to a difference between Needle and the portion of Haystack starting at J, as the for-loop in SPARK does not increment its index in the last iteration of the loop, contrary to its C version.

On this initial version, GNATprove issues one message about a possible integer overflow when computing "Haystack'Length - Needle'Length + 1". It automatically proves all other run-time checks (2 initialization checks, 1 array index check,  2 integer range checks, 2 integer overflow checks). GNATprove also provides a counterexample to understand the possible failure, which can be displayed in our IDE GPS by clicking on the magnify icon on the left of the message/line:

You have to scroll right in the IDE to see all the values, so here are the relevant ones: Haystack'First = 1 and Haystack'Last = 2147483647 and Needle'First = 1 and Needle'Last = 0. In that case, Haystack'Length is 2147483647 and Needle'Length is 0, which means that "Haystack'Length - Needle'Length + 1" is one past the largest signed 32-bits integer. Hence the overflow. One way to avoid this issue is to require that Needle is not the empty string, so its length is at least 1:

This precondition is sufficient for GNATprove to prove all checks in Brute_Force, but I've made it stronger like done by TMM in his post, as it does not make sense to look for a needle that is longer than the haystack:

Note that, compared to what is needed with Frama-C, we don't need here to provide loop assigns or loop invariants. GNATprove automatically computes the variables that are modified in a loop, as well as the range of for-loop indexes. Still following the order of exposure of TMM's posts, let's turn to the functional contract for searching a string. I'm directly translating here the functions partial_match_at and match_at given by TMM from C to SPARK, as well as the contract of brute_force. Functions Partial_Match_At and Match_At are ghost functions in SPARK (with aspect Ghost), which means that they can be used only in assertions/contracts and ghost code. A difference with Frama-C is that ghost code is executable like regular code in SPARK, so one must show absence of run-time errors in ghost code as well, hence the precondition on Partial_Match_At below:

The contract on Brute_Force is similar to the one in Frama-C, with a shift by one for the origin of strings, Brute_Force'Result instead of \result to denote the result of the function, and an if-expression instead of behaviors (SPARK has a similar notion of contract cases, but they must always have disjoint guards in SPARK, so are not applicable here):

Before we even try to prove that this contract is satisfied by the implementation of Brute_Force, it is a good idea to test it on a few inputs, to get rid of silly mistakes. Here is a test driver to do precisely that:

with String_Search; use String_Search;

Just compile the code with assertions on (switch -gnata), run it, and... it fails the precondition of Brute_Force:

What happened here is that I put arguments in the wrong order in the call to Brute_Force. I'm not making this up, this really happened to me (I am that bad!). Anyway, that illustrates that testing is a good idea, even if here it detected a bug in the test itself. The fix in SPARK is to use named parameters to avoid such issues. They don't have to appear in the same order as in the function signature, but it's a good idea nonetheless:

Once fixed, the test passes without errors. Like in the case of Frama-C, we need to add loop invariants for GNATprove to prove that Brute_Force satisfies its contract. Loop invariants in SPARK are different from the classical loop invariants used in Frama-C: you can put them anywhere in the loop, and they don't have to hold when reaching/exiting the loop but only when execution reaches the program point of the loop invariant. I prefer in general to put loop invariants at the end of loops, because it's more natural to express what has been achieved so far:

A subtlety above is that, since we're replacing the implicit loop invariant in the inner loop (located at the start of the loop) by an explicit loop invariant at the end of the inner loop, we need to repeat in that loop invariant the information about the current value of Diff, otherwise this information is not available on the path starting from the loop invariant and exiting the loop in the last iteration. Otherwise this is similar to what was done in Frama-C. With these loop invariants, GNATprove proves all checks in Brute_Force, including its postcondition.

I kept above the implementation structure originating from the C version of brute_force, but in SPARK we can simplify it by replacing the inner loop with a direct comparison of Needle with a slice of Haystack:

This version is also completely proved by GNATprove.

Now turning to the more involved algorithm for string search called quick search presented in this other post by TMM. Translating the implementation, contracts and loop invariants in SPARK is quite easy. As for the brute force version, more precise types in SPARK allow to get rid of a number of annotations:

I am also getting rid of a loop in Make_Bad_Shift and a loop in QS compared to their C version, as we can directly assign and compare strings in SPARK:

GNATprove proves all checks on the above code, including postconditions, except for the array index check when computing "Haystack(I + Needle'Length)". This is precisly the bug that was discovered by TMM, that he presents in his post. GNATprove further helps by providing a counterexample to understand the possible failure:

Indeed, when I=2 and Haystack'Last=2, "I + Needle'Length" is outside of the bounds of Haystack whenever Needle is not the empty string. We can fix that by exiting early from the loop before the assignment to I in the loop:

With this fix, GNATprove proves all checks on the code of quick search.

Now turning to proving the functional behavior of quick search. The postcondition of QS is the same as the one of Brute_Force, given that only the algorithm changes between the two:

In order to prove the contract of QS, we'll need to specify and prove the functional behavior of Make_Bad_Shift first. As explained by TMM in his post, Make_Bad_Shift is used to align the last instance of a given character in the needle with a matching character in the haystack. So for every such character C, either it does not occur in the needle in which case Bad_Shift(C) has the value "Needle'Length + 1", or it occurs (possibly multiple times) in the needle in which case it occurs last at index "Needle'Length - Bad_Shift(C) + 1". This is what is expressed in the following postcondition:

In order to prove that the implementation of Make_Bad_Shift satisfies this postcondition, we simply have to repeat this postcondition as a loop invariant, accumulating that information as the loop index J progresses (see how occurrences of Needle'Last in the postcondition were replaced by occurrences of J in the loop invariant):

GNATprove proves all checks on the above code.

Now turning to QS, we need to establish a loop invariant very similar to the one used in Brute_Force, except here we want to establish the property that Needle does not match up to index "I + Bad_Shift(Haystack(I + Needle'Length)) - 1" instead of just I:

We also need to bound I in the loop invariant, as we're inserting the above loop invariant in the middle of the loop, hence we do not get "for free" that I satisfies the loop test:

With these additions, GNATprove proves all checks in QS, including its postcondition, but it does not prove its loop invariant:

This is expected. There is a big reasoning gap to go from the postcondition of Make_Bad_Shift to the loop invariant in QS. We are going to use ghost code to close that gap and convince GNATprove that the loop invariant holds in every iteration. What we need to show is that, for every starting position that is skipped (for K in the range I + 1 to I + Bad_Shift(Haystack(I + Needle'Length)) - 1), the needle cannot align with the haystack at that position. In fact, we know exactly at which position these alignments would fail: at the position "I + Needle'Length" in Haystack. Looking at the postcondition of Make_Bad_Shift, this corresponds to position "I + Needle'Length - K + 1" in Needle. Let's write it down just before the loop invariant:

GNATprove proves the above assertions, using the first one to prove the second one, so we can now accumulate this information in a loop invariant for all values of positions that are skipped:

With this addition of ghost code, GNATprove proves all checks in QS, including its postcondition and loop invariants. In the final version of that code, I'm using a local ghost procedure Prove_QS instead of inlining the ghost code in the implementation of QS. That way, GNATprove still internally inlines the implementation of Prove_QS to prove QS, but the compiler will completely get rid of the body and call to Prove_QS in the final executable built without assertions:

I also added a loop variant to ensure that the while-loop will terminate. For-loops always terminate in SPARK because the loop index cannot be assigned by the user (contrary to what C allows), but while-loops or plain-loops might not terminate, hence the use of a loop variant to verify their termination.

The code presented in this post is available on GitHub: spec and body. Now a challenge for Frama-C users is to translate back the functional proof of QS in SPARK into C and Frama-C!

The project SPARK-by-Example by Christophe Garion and Jérôme Hugues contains other examples of functionally proven string algorithms, which correspond to the SPARK version of the work done by Jens Gerlach with Frama-C in the ACSL-by-Example project.