如何用coq证明c程序的正确性

Question

我想证明我的一些程序的正确性，但我不知道从哪里开始。假设我有以下程序，我如何证明它的正确性或不存在。我如何从下面的源代码中将它们插入定理证明器中。 Coq 或 ACL2 或几乎任何东西。

下面的代码仅计算从标准输入读取的字节数。它有 2 个版本，一个版本进行逐字节计数，另一个版本在可能的情况下按无符号整数大小的块读取它们。我知道它不方便也不美观，这只是一个可以让我开始的例子。在一些帮助下。

代码有效，我知道它是正确的，我知道如何为其编写单元测试，但我不知道如何证明它。

#include <stdio.h>
#include <unistd.h>
#include <stdlib.h>

unsigned count_bytes1(unsigned char * bytes, unsigned len) {
    unsigned count=0;
    unsigned i;
    for (i=0;i<len;i++) {
        count+=bytes[i];
    }
    return count;
}
unsigned count_word(unsigned word) {
    unsigned tmp = word;
    if (sizeof(unsigned)==4) {
        tmp = (0x00FF00FFU&tmp) + (( (0xFF00FF00U)&tmp)>>8);
        tmp = (0x0000FFFFU&tmp) + (( (0xFFFF0000U)&tmp)>>16);
        return tmp;
    }
    if (sizeof(unsigned)==8) {
        tmp = (0x00FF00FF00FF00FFU&tmp) + (( (0xFF00FF00FF00FF00U)&tmp)>>8);
        tmp = (0x0000FFFF0000FFFFU&tmp) + (( (0xFFFF0000FFFF0000U)&tmp)>>16);
        tmp = (0x00000000FFFFFFFFU&tmp) + (( (0xFFFFFFFF00000000U)&tmp)>>32);
        return tmp;
    }
    return tmp;
}
unsigned count_bytes2(unsigned char * bytes, unsigned len) {
    unsigned count=0;
    unsigned i;
    for (i=0;i<len;) {
        if ((unsigned long long)(bytes+i) % sizeof(unsigned) ==0) {
            unsigned * words = (unsigned *) (bytes + i);
            while (len-i >= sizeof(unsigned)) {
                count += count_word (*words);
                words++;
                i+=sizeof(unsigned);
            }
        }
        if (i<len) {
            count+=bytes[i];
            i++;
        }
    }
    return count;
}

int main () {
    unsigned char * bytes;
    unsigned len=8192;
    bytes=(unsigned char *)malloc(len);
    len = read (0,bytes,len);
    printf ("%u %u\n",count_bytes1(bytes,len),count_bytes2(bytes,len));
    return 0;
}

Answer 1

1.知道你要证明什么：规范

首先，决定您想要为您的函数证明什么。例如，使用 ACSL 规范语言为您的函数编写合约：

/*@ ensures \result >= x && \result >= y; 
    ensures \result == x || \result == y; 
*/ 
int max (int x, int y);

2.验证

然后，您可以证明您的实现满足规范，例如使用 Frama-C 的 WP 插件。

WP插件将生成证明义务，验证义务将确保实施符合规范。如果你觉得有趣的话，你可以在 Coq 8.4+ 中证明这些（但几乎没有人真正这样做时不会首先应用可用的全自动 SMT 证明器，例如 Alt-Ergo）。

---

PS：看来您正在尝试证明一个 C 函数与另一个 C 函数等效，即使用一个简单的 C 函数作为优化函数的规范。本文采用的方法是证明一个与另一个的等价性：

何塞·巴塞拉尔·阿尔梅达、曼努埃尔·巴博萨、豪尔赫·苏萨·平托和芭芭拉·维埃拉。 验证加密软件相对于参考实现的正确性。 FMICS’09，LNCS 第 5825 卷，第 37-52 页，2009 年。

Answer 2

一个更基本的问题是，据称包含非平凡 C 程序的文件实际上是否包含有效的 C 程序。不仅是 ANSI C 规范中的必须条件，还包括所有应该和不应该条件。通常我们的编译器会被指责无法正常工作，但是当开发人员查看源“代码”时，他们发现它不包含 C。请注意，编译器和运行时应该强制执行所有必须条件，但是当违反“应该”条件是未定义的。人们可以在检测到这种情况时发布代码来删除所有用户文件。当然，有信誉的编译器不会这样做，但并不禁止。通常，在低选项下，人们期望生成的代码会按照您的预期进行操作，但在高选项下编译的代码可能会输出完全垃圾。就我个人而言，我通常不会以高选项编译生产 C 应用程序，而只会使用适度的代码优化，因为很难确定编写的代码实际上是有效的 C，而且我多次阅读了 ANSI C 规范。