- c - 在位数组中找到第一个零
- linux - Unix 显示有关匹配两种模式之一的文件的信息
- 正则表达式替换多个文件
- linux - 隐藏来自 xtrace 的命令
我想证明我的一些程序的正确性,但我不知道从哪里开始。假设我有以下程序,我如何证明它的正确性或不正确。我怎样才能从下面的源代码中将它们插入定理证明器。 Coq 或 ACL2 或几乎任何东西。
下面的代码只是计算它从标准输入中读取的字节数。它有 2 个版本,一个按字节计数,另一个在可能的情况下按无符号整数大小的 block 读取它们。我知道它不便携也不漂亮,它只是一个可以让我开始的例子。在一些帮助下。
代码有效,我知道它是正确的,我知道如何为它编写单元测试,但我不知道如何证明它。
#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;
}
最佳答案
首先,确定您要为您的函数证明什么。例如,使用 ACSL 为您的函数编写合约规范语言:
/*@ ensures \result >= x && \result >= y;
ensures \result == x || \result == y;
*/
int max (int x, int y);
然后,您可以证明您的实现满足规范,例如使用 Frama-C 的 WP plug-in .
WP 插件将生成证明义务,其验证将确保实现相对于规范是正确的。如果您觉得有趣,您可以在 Coq 8.4+ 中证明这些(但几乎没有人真正这样做不是首先应用可用的全自动 SMT 证明程序,例如 Alt-Ergo)。
PS:您似乎在试图证明一个 C 函数等价于另一个,也就是说,使用一个简单的 C 函数作为优化函数的规范。证明一个相对于另一个的等价性是本文遵循的方法:
José Bacelar Almeida、Manuel Barbosa、Jorge Sousa Pinto 和 Bárbara Vieira。验证关于引用实现的加密软件的正确性。 FMICS’09,LNCS 第 5825 卷,第 37-52 页,2009。
关于c - 如何用coq证明c程序的正确性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/16141108/
(这不是关于定理证明,而是关于实践中的测试,例如 quickCheck) 让f一些通用函数 f :: RESTRICTIONS => GENERICS 具有一些“理想的”属性(即不是 hack,是不可
给定数组 arr 和索引数组 ind,以下算法就地重新排列 arr 以满足给定的索引: function swap(arr, i, k) { var temp = arr[i]; arr[i]
我有兴趣创建一个具有运行时间和空间限制的简单数组问题。看来我找到了解决问题的方法。请阅读以下java代码中问题的初始描述注释: /* * Problem: Given two integer ar
我是 isabelle 的新手,并试图证明以下简单的不等式: lemma ineq: "(a::real) > 0 ⟹ a 0 ⟹ b 0" proof have "1/a + 1/b >
是否有任何理论说缓存应该比文件系统更快? 我认为,由于文件系统也使用缓存,因此没有科学证据表明当文件系统的概念有些松散时,我们应该将内容从文件系统移动到诸如 memcache 之类的缓存中——比如下载
我正在做一个证明,我的一个子目标看起来有点像这样: Goal forall (a b : bool) (p: Prop) (H1: p -> a = b) (H2: p), neg
我有定义的归纳类型: Inductive InL (A:Type) (y:A) : list A -> Prop := | InHead : forall xs:list A, InL y (co
我知道 CRC 是一个线性函数,这意味着 CRC(x xor y) = CRC(x) xor CRC(y),但我不知道如何证明 CRC 的这个属性。 有谁有想法吗? 非常感谢! 最佳答案 这通常不是真
我是 Coq 的初学者。 虽然计算机为我验证了证明令人满意,但众所周知,满足 Coq 的证明对人类来说难以阅读。这是一个简单的例子,假设您没有看到任何评论: Theorem add_comm : fo
我试图了解是什么决定了类型参数是否必须是标称的。 虽然 GADT 和类型家族在某种意义上看起来不同,但它们不是“简单容器”,因为它们的实例定义可以“查看”它们的参数,但简单类型是否可以明显需要名义参数
我想使用 function 关键字定义来证明函数定义的正确性。以下是自然数的通常归纳定义上的加法函数的定义: theory FunctionDefinition imports Main begin
我定义了一个 Sygma-Type,如下所示: { R : nat -> nat -> bool | Reflexive R } 我有两个元素 r1 r2 : { R : nat -> nat ->
我有以下数据: new_pairs x y Freq start.latittude start.longitude start.station end.la
出于教育目的,我一直试图通过使用各种语言扩展和单例类型,在 Haskell 中重建《Type-Driven Development with Idris》(即 RemoveElem.idr )一书中的
我定义了一个 Sygma-Type,如下所示: { R : nat -> nat -> bool | Reflexive R } 我有两个元素 r1 r2 : { R : nat -> nat ->
我正在使用Ax DevTools,并且试图弄清楚如何使用相同的构建信息标记多个扫描。现在,我的测试运行如下: class MyTestCase : XCTestCase { func myTest
我正在尝试证明一个函数的正确性,该函数检查数组是否按递增/递减顺序排序或未排序。行为是返回 -1,如果按降序排序,1,如果按升序排序,大小为 1,或包含相同的值,0,如果没有已排序或为空。运行:Fra
我试图证明 Z3(Microsoft 的 SMT 求解器)中的一个归纳事实。我知道 Z3 通常不提供此功能,如 Z3 guide 中所述。 (第 8 节:数据类型),但是当我们限制要证明事实的域时,这
问题已编辑: 如代码中所述,HashSet 和 HashMap 是快速失败的(但这不是保证): void goHashSet() { Set set = new HashSet();
我试图使导航栏中的链接延伸到导航栏的全长。我环顾四周,发现了一些有用的信息,但无法使其正常工作 HTML: To
我是一名优秀的程序员,十分优秀!