c - 检查数组是否按升序或降序排序的函数的 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] 可能使两个谓词都返回 true，这会使 Frama-c 感到困惑。

我想修改谓词 is_sortedDec(t,size) 以表达以下想法:数组按降序排序并确保该属性，至少有 2 个索引 x，y 例如 array[x] !=数组[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 ，这样调用者可能会错误地得出数组已排序的结论。