如何使用Coq证明C程序的正确性

Question

我想证明一些程序的正确性，但不知道从哪里开始。假设我有以下程序，如何证明其正确性或错误性。我该如何将下面的源代码插入到定理证明器中，例如Coq或ACL2或几乎任何其他工具。

以下代码仅计算从标准输入读取的字节数。它有两个版本，一个是逐字节计数，另一个是尽可能使用无符号整数大小块进行读取。我知道它不可移植或优美，这只是一个可以帮助我入门的示例。

该代码可以工作，我知道它是正确的，并且我知道如何为它编写单元测试，但我不知道如何证明它的任何内容。

#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;
}

- Martin

---

你所谈到的“正确性”，很难保证，因为在执行和代码之间有编译器。你必须确保编译器也能生成保持正确性的代码。你还提到了可移植性，不过这也不能排除在外。不同的架构有不同的类型大小。我相当确定你需要将你的集合限制在特定的编译器（版本）、特定的架构、特定的操作系统等方面，才能使其有可能证明任何东西。 - Jite

你的代码是否假定char恰好为8位？看起来是这样。 - autistic

我知道这个小例子没有考虑很多东西，但我可以加以考虑。我不想证明这个例子。我想学习如何通用地做它。这个例子只是一个起点示例。我知道有些软件已被证明正确，我也想能够做到这一点。 - Martin

假设我们可以做出以下假设：已经定义了C或C++标准或标准的子集，我们有一个可靠的编译器，我们有一台能够正确执行机器码的计算机。那么，我们如何证明程序本身是正确的？我们如何定义“正确”的含义？首先，我们可以假设“正确”意味着count_bytes1和count_bytes2始终返回相同的结果。 - Martin

你需要首先定义程序。上面的代码不是特定程序定义的示例，因为输出因系统而异。除非程序的定义允许这种变化，否则该程序就无法“正确”。 - autistic

如何定义程序？ - Martin

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）。

---

另外，您似乎正在尝试证明一个 C 函数等价于另一个 C 函数，也就是使用一个简单的 C 函数作为优化函数的规范。本文采用了一种以其中一个函数为基准并验证其相对于另一个函数的等价性的方法：

José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, and Bárbara Vieira. Verifying cryptographic software correctness with respect to reference implementations. In FMICS’09, volume 5825 of LNCS, pages 37–52, 2009.

- Pascal Cuoq