如何用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 %un",count_bytes1(bytes,len),count_bytes2(bytes,len));
    return 0;
}

Answer 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函数作为一个优化函数的规范。证明一个相对于另一个的等价性是本文所采用的方法:

约瑟·巴塞拉尔·阿尔梅达，曼努埃尔·巴博萨，豪尔赫·索萨·平托，Bárbara维埃拉。根据参考实现验证加密软件的正确性。