Я пытаюсь доказать правильность функции, которая проверяет, отсортирован ли массив в порядке возрастания/убывания или не отсортирован. Поведение должно возвращать -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;
}
}
}
}
Вот логика.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] может привести к тому, что оба предиката вернут true, что сбивает с толку 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 был не слишком доволен синтаксисом.
Любая идея о том, как я могу решить эту проблему? И, может быть, улучшает общее доказательство? Спасибо.
