ACSL proof of a function that checks if an array is sorted in increasing or decreasing order

Question

I'm trying to prove the correctness of an function that checks if an array is sorted in increasing/decreasing order or not sorted. The behaviour is to return -1 if sorted in decreasing order, 1 if sorted in increasing order, of size 1, or containing the same value and 0 if no sorted or empty. To run: Frama-c-gui -wp -wp-rte filename.c

#include "logics.h"
#include <stdio.h>

/*@
requires size > 0;
requires \valid (t +(0..size-1));
ensures \forall unsigned int i; 0 <= i < size ==> (t[i] == \old(t[i]));
ensures size == \old(size);
ensures \result == -1 || \result == 0 || \result == 1;
ensures is_sortedInc(t,size) ==> (\result == 1);
ensures is_sortedDec(t,size) ==> (\result == -1);
ensures not_sorted(t,size) ==> (\result == 0);
ensures size <= 0 ==> (\result == 0);
ensures size == 1 ==> (\result == 1);
assigns \nothing;
*/
int isSortedIncDec (int * t, unsigned int size){
    if (size <= 0){
        return 0;
    }
    else if (size == 1)
    {
        return 1;
    }
    else
    {
        unsigned int i = 0; 
        /*@
        loop assigns i;
        loop invariant 0 <= i <= size-1;
        loop invariant \forall unsigned int j; 0 <= j < i < size ==> t[j] == t[i];
        loop variant size - i;
        */
        while ( i < size - 1 && t[i] == t[i+1] )
        {
            i++;
        }

        if (i == size-1)
        {
            return 1;
        }

        else
        {
            if (t[i] < t[i+1])
            {   
                /*@
                loop assigns i;
                loop invariant 0 <= i <= size-1;
                loop invariant \forall unsigned int j; (0 <= j < i < size - 1) ==> (t[j] <= t[i]);
                loop variant size - i;
                */
                for (i+1; i < size-1; i++)
                {
                    if (t[i] > t[i+1])
                    {
                        return 0;
                    }
                }
                return 1;
            }

            if (t[i] > t[i+1])
            {   
                /*@
                loop assigns i;
                loop invariant 0 <= i <= size-1;
                loop invariant \forall unsigned int j; (0 <= j < i < size - 1) ==> (t[j] >= t[i]);
                loop variant size - i;
                */
                for(i+1 ; i < size-1; i++)
                {
                    if (t[i] < t[i+1])
                    {
                        return 0;
                    }
                }
                return -1;
            } 
        } 
    }
}

Here is logics.h:

#ifndef _LOGICS_H_
#define _LOGICS_H_
#include <limits.h>


/* Informal specification: 
    Returns -1 if an array 't' of size 'size' is sorted in decreasing order
    or 1 if it is sorted in increasing order or of size 1
    or 0 if it is either not sorted, empty or of negative size.
    Note that an array filled with only one value is considered sorted increasing order ie [42,42,42,42].
 */

/*@
lemma limits:
    \forall unsigned int i;  0 <= i <= UINT_MAX;

predicate is_sortedInc(int *t, unsigned int size) =
\forall unsigned int i,j; ( 0<= i <= j < size ) ==> t[i] <= t[j];

predicate is_sortedDec(int *t, unsigned int size) =
\forall unsigned int i,j; ( 0<= i <= j < size ) ==> t[i] >= t[j];


predicate not_sorted(int *t, unsigned int size)=
\exists unsigned int i,j,k,l; (0 <= i <= j <= k <= l < size) ==> (t[i] > t[j] && t[k] < t[l]);

*/

#endif

The issue comes from Frama-c failing to prove the postconditions:

ensures is_sortedInc(t,size) ==> (\result == 1);
ensures is_sortedDec(t,size) ==> (\result == -1);

It's an expected problem as the predications overlap in the case of the array containing the same value, meaning an array [42,42,42] could make both predicates return true, which confuses Frama-c.

I would like to modify the predicate is_sortedDec(t,size) to express the following idea: the array is sorted decreasingly and with that property ensured, there is at least 2 indexes x,y such as array[x] != array[y].

There exists two indexes x,y such that t[x] != [y] and the array is sorted in decreasing order for all indexes.

I've tried something like this:

predicate is_sortedDec(int *t, unsigned int size) =
\forall unsigned int i,j; ( 0<= i <= j < size ) 
==> (t[i] >= t[j] 
    && (\exists unsigned int k,l ; (0<= k <= l < size) ==> t[k] != t[j]) );

but Frama-c wasn't too happy about the syntax.

Any idea about how I could solve this issue? And maybe improves the overall proof? Thanks.

Answer 1

I'm not sure of what you mean by "Frama-C wasn't too happy about the syntax". Your predicate looks syntactically correct to me, and to my Frama-C version as well.

Semantically, though, there is indeed an issue: you shouldn't use the implication (==>) but a conjunction (&&) under the existential quantifier. Otherwise, any size<=k<=l would be a witness satisfying the formula.

More generally, you almost always use quantifications like \forall x, P(x) ==> Q(x) and \exists x, P(x) && Q(x). Indeed, the former reads "for any x, if P(x) holds, then Q(x) holds, while the latter is "I want to find an x verifying both P(x) and Q(x). If you replace the conjunction by an implication, you're asking for an x such that if P(x) holds then so is Q(x), which can be achieved (in classical logic at least) by finding an x for which P(x) does not hold.

That said, automated provers often have difficulties with existential quantifiers (because they basically have to exhibit some witness for the formula), and according to your informal spec, there there is a pair (k,l) which is obvious: 0 and size-1. Of course, you need for that to add to your predicate the condition that size>=2, but you need it anyway, else you would face the same issue that both predicates are true for a single-element array. By the way, you probably also need to add size>=1 in the is_sortedInc predicate as well. Otherwise, the predicate will be true for size==0 (a universal quantification over an empty set of values is always true), but your function returns 0 in that case, so that the corresponding ensures does not hold.

I haven't checked your loop invariants in detail, but they look quite reasonable.

UPDATE Based on your comment below, your new version of the predicates still makes some confusion on the use of connectors and quantifiers:

• the conditions on size itself should be outside of any quantifier.
• In isSortedDec, you should have an implication under the forall and a conjunction under the exists, which itself should not be under the forall.

To summarize, the predicates should rather look like

predicate is_SortedInc(int *t, unsigned int size) =
  size > 0 &&
  \forall unsigned int i,j; ( 0<= i <= j < size ) ==> t[i] <= t[j];

predicate is_sortedDec(int *t, unsigned int size) =
  size > 1 &&
  \forall unsigned int i,j; ( 0<= i <= j < size ) ==> t[i] >= t[j] &&
  \exists unsigned int i,j; (0<=i<j<size) && t[i] < t[j];

Furthermore, if you remove the not_sorted post-condition, then you basically allow the function to return anything in this case, including 1 or -1, so that a caller might conclude wrongly that the array is sorted.