问题标签 [proof-of-correctness]

假设我有

以及该类型的谓词，

这不适用于Banana,Orange和Lemon其他。

可以说this 定义WineStock为 ; 上的谓词Fruit。WineStock Grape为真（因为我们可以构造该类型的值/证明：）CanonicalWine以及WineStock Apple，但WineStock Banana为假，因为该类型不包含任何值/证明。

那么，我怎样才能有效地使用Not (WineStock Banana),Not (WineStock Lemon)等呢？似乎对于除and之外的每个Fruit构造函数，我不得不编写一个 case split over ，某处，充满s：GrapeAppleWineStockimpossible

注意：

• 代码重复，
• 当谓词定义增长时，LoC 会爆炸，获得更多的构造函数。想象一下这个Not (Sweet Lemon)证明，假设定义中有许多甜蜜的选择Fruit。

所以，这种方式似乎不太令人满意，几乎不切实际。

有更优雅的方法吗？

有一些方法（例如，https: //jeltsch.wordpress.com/2012/04/30/dependently-typed-programming-and-theorem-proving-in-haskell/ ，PromotedDataKinds 扩展）在haskell中伪造依赖类型，这使得在 haskell 本身中证明一些代码属性成为可能。

我可能想要证明的属性示例包括某些函数的整体性或 somr Monad 类型类实例的 monad 法则。

这样的证明将是一个值 (a::T)，其中 T 代表我们已经证明的陈述。不幸的是，在 haskell 中，我们可以编写错误类型的术语，例如 (fix id::forall aa)，因此我们实际上可以证明一切。是否有工具可以检查 Haskell 中的证明正确性或单子定律满意度？有人在源代码中包含证明吗？

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

这是算法：

我做了一些研究并将不变量缩小到if x is in a[0 .. n-1] then a[l] <= x < a[r].

我不知道如何从那里取得进展。前提条件似乎太宽泛了，所以我很难证明P -> I.

非常感谢任何帮助。这些是可以用来证明算法正确性的逻辑规则：

我被困在以下问题问题陈述中。我已经考虑了一段时间，然后查看了问题的一些线索，因为我无法提出解决方案。我的理解是，这是“装箱”问题的一个特例，通常是 NP-Hard。尤其是查看 CodeForces Blog Idea的这个想法，我无法理解为什么这在这里甚至可以达到最佳效果。特别是我们如何证明这个算法是最优的？

问题陈述 ：

恩佐正在装修他的新房子。最困难的部分是购买正确数量的瓷砖。他想要 N 个不同大小的瓷砖。当然，它们必须从他买的瓷砖上切下来。所有需要的瓷砖都是方形的。瓦片边长为 2^S1, 2^S2, ..., 2^SN。他只能买很多 M*M 大小的瓷砖，为了方便起见，他决定只切割平行于侧面的瓷砖。他需要买多少块瓷砖？

离散数学很有趣，但我对所涉及的代数仍然有很多困难。我试图通过归纳来证明递归函数。我刚刚开始我的算法设计课程，任务是将迭代函数重写为递归函数，然后证明它。我能够实现递归函数，并且能够使用蛮力技术对其进行测试，但我不知道如何设置我的证明。我认为我没有正确启动它。我在证明中加入了我的开始。感谢您能给我的任何指示。

编辑＃3最终证明完成感谢帮助

编辑#2 这是我迄今为止的证明，我相信我已经很远了。

下面是我的代码：

A colleague of mine has written a program that proves that some conditions will not be met after testing an algorithm running multiple concurrent threads trying to find a sequence that might trigger the unwanted condition. He used a computer language that was designed for this purpose, but I can't remember its name. What are the languages that serve this specific purpose?

The ultimate in optimizing compilers would be one that searched among the space of programs for a program equivalent to the original but faster. This has been done in practice for very small basic blocks: https://en.wikipedia.org/wiki/Superoptimization

It sounds like the hard part is the exponential nature of the search space, but actually it's not; the hard part is, supposing you find what you're looking for, how do you prove that the new, faster program is really equivalent to the original?

Last time I looked into it, some progress had been made on proving certain properties of programs in certain contexts, particularly at a very small scale when you are talking about scalar variables or small fixed bit vectors, but not really on proving equivalence of programs at a larger scale when you are talking about complex data structures.

Has anyone figured out a way to do this yet, even 'modulo solving this NP-hard search problem that we don't know how to solve yet'?

Edit: Yes, we all know about the halting problem. It's defined in terms of the general case. Humans are an existence proof that this can be done for many practical cases of interest.

如果我有一个So类型，比如So (x < y)，由类似的东西创建

我怎样才能从中提取证据(x < y)？我在标准库中找不到这个函数。

So在标准库中定义为：

而且我不确定如何从中提取证据，以用于证明以下内容：

抱歉，我希望这对于 stackoverflow 来说不是太遥远。我有一个算法，我想证明它是正确的，或者如果不是，请找到一个反例。

这是问题所在。我有一组严格的正权重：w1、w2、w3、... wn。

我有一个长度为 m 的布尔向量，其中 m>n。向量必须恰好有 n 个真值和 mn 个假值。

例如，如果 m=5 且 n=3，则 v 可以是 (1, 1, 0, 1, 0)

接下来，我们有将 v 向量映射到自然数的函数：

其中 w[wIndex] 给出权重 w1, w2, w3 ... wn。

Next 考虑 v 的圆周旋转，例如，如果 v=(0, 1, 1, 0, 1) 那么 rotate(v, 3) 是 v 向左旋转了 3 个位置，或者 (0, 1, 0, 1, 1）。圆形旋转保留 m（长度）和 n（个数）。

我们将 minF(v) 定义为 v 的所有可能的圆形旋转中的最小 f 值。它可以实现如下：

其中 rotate(v, k) 将 v 循环旋转 k 个位置

现在我们终于解决了这个问题：

证明或反证 best(m, n) 产生的向量使得 minF(optimum(m, n)) >= minF(w) 对于所有可能的向量 w，长度为 m 和 n 个，其中最优定义如下：

最后，这里有一些优化运行的例子：

Optimum 基本上将它们分散得尽可能远。

我做了很多实证测试，这个算法似乎总是有效，但我真的需要证明它是正确的。

PS如果你解决了这个问题，我给你买披萨。