问题标签 [hoare-logic]

在霍尔逻辑中，人们经常区分部分正确性和完全正确性。部分正确性意味着程序满足其规范，或者不会终止（无限循环或递归）。

有谁知道为什么要引入这种关于终止的微妙之处？对我来说，似乎只有完全正确才有用：程序满足其规范并终止。谁想执行一个可能的无限循环？

我的老师告诉我以下语句是有效的： {x > 3} while true (x := 3) {x = 3}

为什么这个说法有效？是因为后置条件永远不会被检查，还是后置条件现在算作不变检查？

简而言之：当存在无限循环时，后置条件可以是任何东西吗？

那么这将是有效的： {x > 3} while true (x := 3) {x = 0}

Python 单元测试中的假设

Python 是否支持将假设用作测试的前提条件，类似于JUnit为 Java 提供的assumeThat(...)方法。

这很重要，因为Hoare Logic的应用，引用 JUnit：

一组方法，可用于陈述有关测试有意义的条件的假设。失败的假设并不意味着代码被破坏，而是测试没有提供有用的信息。假设基本上意味着“如果这些条件不适用，请不要运行此测试”。默认的 JUnit 运行器会跳过假设失败的测试。自定义跑步者的行为可能不同。

似乎 Python 在其unittest framework中没有提供这些开箱即用的功能。我通过扩展unittest.TestCase.

有了这个行为单元测试：

这种方法似乎表现出我想要的正确行为，这是最好的方法，有没有更好的方法来做到这一点，或者使用 3rd 方库？我正在寻找一种更好的方法，而不是用这种方式包装所有基本断言来做出我自己的假设。

所以，我写了一个快速排序算法和一个 hoare-partition 算法。不知何故，当我尝试在 main() 中运行示例案例时，它挂断了 quickSort(test, 0,3)。似乎有一个无限循环。我不知道如何解决它，因为这两个功能似乎都很好。

我尝试调试，但我对 c 相当陌生。我注意到 quickSort(test,0,3) 递归调用自己。所以我知道这个问题与高而不是减少有关。但是我从大学幻灯片中获取了示例伪代码来构建该功能，并且一切似乎都排成一行。

我实际上希望打印出的测试数组是这样排序的：“9, 24, 30, 42, 64, 81, 90, 95”

正如标题所说，如何使用 Hoare Triple 验证以下功能？我阅读了有关它的各种讲座，但我不知道该怎么做。

在哪里可以找到更复杂的使用 Hoare 逻辑来验证 Isabelle/HOL 中的程序的示例？

我最近了解了在 Isabelle/HOL 中使用 Hoare 逻辑进行程序验证的这一方面。我发现本教程中的示例是简单的示例（http://www.inf.ed.ac.uk/teaching/courses/ar/HoareLogicLecture.thy）。在哪里可以找到更复杂的使用 Hoare 逻辑来验证 Isabelle/HOL 中的程序的示例？

我试图证明选择排序的正确性，其中我应该只使用数学谓词逻辑来证明程序的正确性，我发现很难将下面给出的英语语句写成谓词并继续证明正确性遵循推理规则，

我必须在谓词中写的语句是，

1. a[0...i-1]已排序

2. 中的所有条目a[i..n-1]都大于或等于 中的条目a[0..i-1]。

我需要证明的程序是

而且我需要证明（这里的P应该是上面的程序）是有效的，我能做的就是证明它的部分正确性，但是如何证明它的全部正确性呢？

这是我对部分正确性的证明：

如何通过 Hoare 逻辑证明具有 while 循环的程序的正确性。有人用任何例子开发它会很有趣，因为我要解决的问题是：

前提条件={n>0}

后置条件={sum=1+2+...+n}

没有必要开发这个例子。我只需要了解该过程，因为我没有实际示例。谢谢你的时间。

我试图使用 Hoare 分区方案编写快速排序算法。我很确定我的分区功能是正确的。我使用变量“交换”来指示左枢轴向右移动和右枢轴向左移动。Sort 函数适用于其他 Partition 算法，所以我认为这也很好。然而我得到了错误。