cannot prove function in frama-C

Question

I am having a problem regarding the function proving in frama C. my code used for proving looks like this :

#include <limits.h>
/*@ 
    requires len>=0 && \valid(arr + (0 .. len-1));
    ensures 0<= \result < len;
    ensures \forall integer j; 0 <= j < len ==> arr[j] < \result;
    assigns \nothing;
*/

int find_min(int* arr, int len)
{
   int min;
   min=arr[0];
    /*@ 
        loop invariant \forall integer j; 0 <= j < i ==> arr[j] < min;
        loop invariant 0 <= min < i <= len;
        loop assigns min , i;
        loop variant len -i;
    */
    for (int i = 0; i < len; i++)
    {
        if (arr[i] < min)
        {
            min = arr[i];
        }
    }
    return min;
}

void main (void)
{
    int a[] = {3, 5, 18, 12, 12};
    int r = find_min(a, 5);
    //@ assert r == 3;
}

This is a program that tries to look for smallest array value. The result of the program will be used to prove if the variable fulfills the conditions that is used in frama-C.

I am currently stuck at this invariance here :

I have done various methods before reaching this conclusion, including changing the "ensures..", but whenever I do that the proved goals will reduce from 13/14 to 12/14, therefore I am currently unsure what to change to increase the prove goals to 14/14. I really need help regarding this because I am really new to frama C. Any response regarding this problem is really appreciated.

Answer 1

There are indeed several issues in your specification. First, the main ensures clause is at odds with what you describe:

tries to look smallest array value

implies that you want something like \result < arr[j]. Moreover, since this is supposed to be the smallest, there should be an index for which the equality holds, i.e. you should use <= rather than <. All in all, we should have

ensures small_value: \forall integer j; 0 <= j < len ==> \result <= arr[j]

(NB: it's always a good thing to give a name (here small_value) to your clauses, it makes it easier to identify them in the logs)

Moreover, you're returning the smallest value, not the index thereof, hence your first ensures clause is incorrect.

Finally for the contract, there's a small issue in the requires clause as well, which will only become apparent if you use -wp-rte to ensure that there are no runtime errors in addition to verifying the contract itself: since you always look at arr[0], you cannot have an empty array, i.e. you must have len > 0.

Now, let's have a look at the invariant: the first invariant must be updated to reflect the change in the ensures. As mentioned in comments, the second one should only speak about the interval of i, there's no reason for min to be within those bounds. And i can be 0 (in fact, it is 0 when entering the loop).

With all this, you can prove that f fulfills its contract. However, this is not sufficient to prove the assert in main. Namely, small_value only ensures that you return a smaller value, but not the smallest. For that we need another ensures, namely

ensures min_value: \exists integer i; 0<= i < len && \result == arr[i];

and of course the corresponding invariant

loop invariant min_so_far: \exists integer j; 0<= j < i && min == arr[j] || min == arr[0];

(Note that min_so_far needs a special case to take into account the fact that we start the loop with min == arr[0])

To sum up, with the following file

#include <limits.h>
/*@ 
    requires valid_arr: len>0 && \valid(arr + (0 .. len-1));
    ensures small_value: \forall integer j; 0 <= j < len ==> \result <= arr[j];
    ensures min_value: \exists integer i; 0<= i < len && \result == arr[i];
    assigns \nothing;
*/

int find_min(int* arr, int len)
{
   int min;
   min=arr[0];
    /*@ 
        loop invariant small_so_far: \forall integer j; 0 <= j < i ==> min<=arr[j];
        loop invariant min_so_far: \exists integer j; 0<= j < i && min == arr[j] || min == arr[0];
        loop invariant loop_index: 0 <= i <= len;
        loop assigns min , i;
        loop variant len -i;
    */
    for (int i = 0; i < len; i++)
    {
        if (arr[i] < min)
        {
            min = arr[i];
        }
    }
    return min;
}

void main (void)
{
    int a[] = {3, 5, 18, 12, 12};
    int r = find_min(a, 5);
    //@ assert r == 3;
}

and Frama-C 28.0 + Why3 1.6.0 + Alt-Ergo 2.5.2 frama-c -wp -wp-rte example.c proves all the verification conditions.