proof-of-correctness

4热度

3回答

我是新来的辅酶Q，我试图证明这一点...... Theorem andb_eq_orb : forall (b c : bool), (andb b c = orb b c) -> (b = c). 这是我的证明，但我碰到困难时，我得到的目标（假=真 - >假=真）。 Proof. intros b c. induction c. destruct b. refle

0热度

1回答

证明正确的，并征服排序

假设我们有一个排序方法： void DD_sort(int a[], int x, int y, int size_a) { if(x == y){ return; } else if(y == x+1){ if(a[x] > a[y]){ /* swap the content */ return; }

0热度

1回答

循环不变Hoare逻辑

我有一个程序，我应该找到一个循环不变量，然后提供一个证明。 {x>=0 && y>=0} // precondition res:=0; i:=0; while (i<y) do res:=res+x; i:=i+1; od {res:=x*y} //postcondition 唯一合乎逻辑的循环不变对我来说是res<=x*y，这是后置条件简单，但我不认为它最好的一个

1热度

1回答

后缀树根边缘的证明

我想知道如何编写一个证据，证明后缀树中分支或根边的数量等于字符串S的字母大小。假设我们有S = {aaabaac} ，字母表= {a，b，c}，字母大小= 3，那么根边缘（或从根开始的分支）仅仅是3，即a，b和c。或者这可以通过定义来证明吗？我不确定！

2热度

1回答

验证程序的等价性

优化编译器的最终目的是在程序空间中搜索等价于原始程序但速度更快的程序。这已经在实践中用于非常小的基本块：https://en.wikipedia.org/wiki/Superoptimization 听起来很难的部分是搜索空间的指数性质，但实际上它不是;最难的部分是，假设你找到了你想找的东西，你如何证明这个新的，更快的程序与原始程序真的是相同的？上次我研究过它，在某些情况下证明程序的某些属性已经

0热度

1回答

证明程序的正确性

功能递归地查找并从具有整数元素 Min(A, b, e) if (b=e) return A[b] m = (b+e)/2 // floor is taken x = Min(A, b, m) y = Min(A, m +1, e) If(x < y) return x else return y 我的前提是一个阵列返回的最小元素：b和e为大于零的整数

0热度

1回答

葡萄酒贸易贪婪解决方案（SPOJ）的正确性证明？

不要误会我在网上法官上发布问题的问题。我只想知道如何证明解决方案的正确性。以下是Wine trading problem的问题。它说，在单位距离有一排房子，每个房子要么出售或购买葡萄酒。总需求=总供给。在交易中完成的工作是涉及距离的葡萄酒数量。问题是满足所有房屋在最低限度工作中的需求。所提出的解决方案是，第一个卖方（比如从右侧开始）卖给第一个买方（金额= min（卖方，买方））（这是贪婪的选择），

0热度

1回答

Bellman-Ford算法的正确性证明

我正试图学习Bellman-Ford算法，但我被证明正确性困扰。我已经使用Wikipedia，但我根本无法理解证明。我在Youtube上找不到任何有用的东西。希望你们任何人都能简单解释一下。此页"Bellman-ford correctness can we do better"不回答我的问题。谢谢。

2热度

2回答

在伊德里斯，我如何从一个类型中提取证据？

如果我有一个So的类型，比如So (x < y)，通过创造的东西像 IsLt : Ord a => (x: a) -> (y: a) -> Type IsLt x y = So (x < y) 我怎样才能提取(x < y)证明了这件事？我无法在标准库中找到此功能。 So在标准库中定义为： data So : Bool -> Type where Oh : So True 而且我

-1热度

1回答

什么编程语言具有测试并发算法的具体目的？

我的一位同事编写了一个程序，证明在测试运行多个并发线程的算法试图找到可能触发不需要的条件的序列之后，某些条件将不会被满足。他使用了专为此目的而设计的计算机语言，但我不记得它的名字。为此特定目的提供哪些语言？