我正试图证明检查数组是按升序还是降序排序的函数的正确性。行为是返回-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对语法不太满意。
关于如何解决此问题的任何想法？也许可以改善整体证明？谢谢。
我不确定您所说的“ 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，谓词将为true（对空值集的通用量化始终为true），但在这种情况下，您的函数将返回0，因此相应的ensures不成立。
我尚未详细检查循环不变式，但看起来很合理。