c - coqでacプログラムの正しさを証明する方法

Question

いくつかのプログラムの正しさを証明したいのですが、どこから始めればよいかわかりません。私が次のプログラムを持っているとしましょう。その正確性または欠如をどのように証明できますか。以下のソースから、それらを定理証明器にプラグインするにはどうすればよいですか。Coq、ACL2、またはほとんど何でも。

以下のコードは、標準入力から読み取るバイト数をカウントするだけです。2 つのバージョンがあり、1 つはバイトごとにカウントし、もう 1 つは可能であれば符号なし整数サイズのチャンクで読み取ります。ポータブルでもきれいでもないことはわかっています。これは、私が始めるための単なる例です。いくつかの助けを借りて。

コードは機能し、それが正しいことはわかっています。単体テストの書き方も知っていますが、それについて何かを証明する方法もわかりません。

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