ACSL-подтверждение функции, которая проверяет, отсортирован ли массив в порядке возрастания или убывания

Question

Я пытаюсь доказать правильность функции, которая проверяет, отсортирован ли массив в порядке возрастания / убывания или нет. Поведение состоит в том, чтобы вернуть -1, если отсортировано в порядке убывания, 1, если отсортировано в порядке возрастания, размера 1 или содержит то же значение и 0, если не отсортировано или пусто. Бежать: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;
            } 
        } 
    }
}

Вот 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

Проблема возникает из-за того, что Frama-c не может доказать постусловия:

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

Это ожидаемая проблема, поскольку в случае массива, содержащего одно и то же значение, предсказания перекрываются, а это означает, что массив [42,42,42] может заставить оба предиката возвращать истину, что сбивает с толку Frama-c.

Я хотел бы изменить предикат is_sortedDec(t,size), чтобы выразить следующую идею: массив сортируется по убыванию, и с обеспечением этого свойства существует как минимум 2 индекса x,y, например array[x]!= Array[y].

Существует два индекса x,y, такие что t[x]!= [Y], и массив сортируется в порядке убывания для всех индексов.

Я пробовал что-то вроде этого:

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]) );

но Frama-c был не слишком доволен синтаксисом.

Есть идеи, как я могу решить эту проблему? И, может быть, улучшит общее доказательство? Спасибо.

Answer 1

Я не уверен, что вы имеете в виду, говоря "Frama-C не слишком доволен синтаксисом". Ваш предикат выглядит синтаксически правильным для меня, а также для моей версии Frama-C.

Однако с семантической точки зрения проблема действительно существует: не следует использовать импликацию (==>) но союз (&&) под экзистенциальным квантором. В противном случае любойsize<=k<=l был бы свидетелем, удовлетворяющим формуле.

В более общем плане вы почти всегда используете количественные оценки, такие как \forall x, P(x) ==> Q(x) а также \exists x, P(x) && Q(x). Действительно, первое гласит "для любогоx, если P(x) держит, то Q(x) удерживает, а последнее - "Я хочу найти x проверка обоих P(x) а также Q(x). Если вы замените союз импликацией, вы проситеx так что если P(x) так и есть Q(x), что может быть достигнуто (по крайней мере, в классической логике) путем нахождения x для которого P(x) не держит.

Тем не менее, у автоматических доказывающих часто возникают трудности с экзистенциальными квантификаторами (потому что они в основном должны предъявлять какие-то свидетельства формулы), и, согласно вашей неофициальной спецификации, существует пара (k,l) что очевидно: 0 а также size-1. Конечно, вам нужно добавить в свой предикат условие, чтоsize>=2, но он вам все равно нужен, иначе вы столкнетесь с той же проблемой, что оба предиката верны для одноэлементного массива. Кстати, наверное, еще нужно добавитьsize>=1 в is_sortedIncпредикат тоже. В противном случае предикат будет истинным дляsize==0 (универсальная количественная оценка по пустому набору значений всегда верна), но ваша функция возвращает 0 в этом случае, так что соответствующие ensures не держит.

Я не проверял подробно ваши инварианты цикла, но они выглядят вполне разумно.

ОБНОВЛЕНИЕ На основании вашего комментария ниже, ваша новая версия предикатов все еще вносит некоторую путаницу в использование соединителей и квантификаторов:

• условия на size сам по себе должен быть вне какого-либо квантора.
• В isSortedDec, вы должны иметь импликацию под forall и союз под exists, который сам по себе не должен быть под forall.

Подводя итог, предикаты должны выглядеть скорее как

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];

Кроме того, если вы удалите not_sorted постусловие, то вы в основном позволяете функции возвращать что угодно в этом случае, включая 1 или -1, так что вызывающий может ошибочно заключить, что массив отсортирован.