3

我试图证明一个函数的正确性，该函数检查数组是否按递增/递减顺序排序或未排序。如果按降序排序，则返回-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] 可以使两个谓词都返回 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 对语法不太满意。

关于如何解决这个问题的任何想法？也许可以改善整体证明？谢谢。

4

1 回答 1

3

我不确定您所说的“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这样的 ifP(x)成立 then so is ，这可以通过找到一个for which不成立Q(x)来实现（至少在经典逻辑中） 。xP(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后置条件，那么您基本上允许函数在这种情况下返回任何内容，包括1or -1，因此调用者可能会错误地得出数组已排序的结论。

于 2019-12-06T13:09:32.903 回答