问题标签 [formal-verification]

我想知道以下检查点是否在矩形内的算法是否有效。我用自己的直觉开发了它（没有强大的三角/数学基础来支持它），所以我很想听听在这件事上有更多经验的人的意见。

语境：

• 矩形由 4 个点定义。它可以旋转。
• 坐标总是正的。
• 根据定义，如果点与矩形相交，则认为该点位于矩形内部。

假设：

• 使用点和矩形顶点之间的距离（下图）。
• 最大可能的总距离是当点位于一个顶点时（第二张图）。
• 如果该点刚好在矩形之外，则距离会更大（第三张图）。

图表链接：http: //i45.tinypic.com/id6o35.png

算法（Java）：

问题：这是正确的吗？

CQRS 如何处理立即一致模型的后置条件？我意识到这样的事情与最终一致的带有事件源等的系统无关。但是如果我只是想将 vanilla CQRS 应用到一个简单的界面，我将如何编写我的后置条件？CQRS 的想法是否总是假设最终的一致性？

增删改查：

CQRS：

我有两个打包的信号数组，我需要为该属性创建一个属性和相关的断言，以证明这两个数组在某些条件下是相同的。我正在正式验证，该工具无法证明单个属性中的两个完整数组，因此我需要将其拆分为单个元素。那么有没有一种方法可以使用循环为数组的每个元素生成一个属性？目前，我的代码非常冗长且难以导航。

我的代码目前如下所示：

这就是我希望我的代码看起来像的样子：

定理证明工具 z3 需要花费大量时间来解决一个公式，我相信它应该能够轻松处理。为了更好地理解这一点并可能优化我对 z3 的输入，我想查看 z3 在其求解过程中生成的内部约束。从命令行使用 z3 时，如何打印 z3 为其后端求解器生成的公式？

假设我有这样的功能：

这个微不足道的函数总是返回 1。使用带有 -O2 选项的 clang 编译并查看反汇编代码 LLVM 正确将此函数编译为return 1;.

我的问题是：llvm如何做静态值分析？最弱的前置条件技术？价值传播？霍尔的技术？

我知道用于验证程序属性的不同形式验证工具（例如 SPIN 模型检查器）。是否有任何通用工具/方法可用于验证实时嵌入式系统中的时序要求？例如：“此算法必须始终在 50 毫秒内终止”。这种类型的验证通常是如何完成的？

我是一名从未正式学习过算法的程序员，并且一直想填补我学习中的空白。我目前正在阅读一些书籍和在线资料，我从概念上理解大 O，即它的用途，以及不同类别的性能，例如常数、线性、二次等。我可以编写问题并直观地理解不同方法的性能影响。

但是，我一直坚持的事情是算法证明的符号，我不确定在哪里可以找到这部分。我看过的所有书籍都假定这种知识水平。

例如，Skiena's Algorithm Design Manual中的这句话让我很难过：

f(n) = O(g(n)) 表示 c * g(n) 是 f(n) 的上限。

因此存在某个常数 c，使得 f(n) 总是 ≤ c * g(n)，对于足够大的 n（即，对于某个常数 n0，n ≥ n0）。

这是读者应该完成的推论练习：

3n^2 − 100n + 6 = O(n^2)，因为我选择c = 3 且3n^2 > 3n^2− 100n + 6；

我可以理解这两种说法，并且可以从逻辑上看出第二种说法是正确的。我也理解上限的概念，即这是最坏的情况。

但是我被困在简单的事情上，比如上面的内容是什么？

• g(n)

• 对于某个常数 n0，n ≥ n0

总的来说，我无法将各个部分拼凑在一起来理解整个证明。

谁能帮我用简单的英语解析上述陈述，并以对非技术人员有意义的方式展示它们与练习的关系

我正在关注 Daniel Jackson 的优秀著作（软件抽象）中的一个示例，特别是他设置令牌环以选举领导者的示例。

我正在尝试扩展此示例（Ring 选举）以确保令牌（而不是仅限于一个）在规定的时间内传递给所有成员（并且每个成员只被选举一次，而不是多次）。但是（主要是由于我对合金缺乏经验），我在找出最佳方法时遇到了问题。最初我认为我可以与一些运算符一起玩（将 - 更改为 + ），但我似乎并没有完全击中头部。

下面是示例中的代码。我已经用问题标记了一些区域......感谢任何和所有帮助。我正在使用合金 4.2。

有哪些工具可以帮助人们尝试弱序并发？ 也就是说，在自学部分围栏、弱原子、获取/使用/释放语义、无锁算法等方面可以玩什么沙盒？

一个人想要的工具或沙箱将锻炼和强调一个弱有序的线程算法，暴露出算法理论上可能失败的各种方式。例如，在 x86 上物理运行，该工具仍然能够暴露 ARM 类型的故障。

一个开源工具会更好。请指教。

参考：

• C++11 标准草案（PDF，见第 1、29 和 30 条）；
• 汉斯-J。Boehm 的主题概述；
• McKenney、Boehm 和 Crowl 关于这个主题；
• GCC 关于该主题的发展说明；
• Linux 内核关于该主题的注释；
• Stackoverflow 上的相关问题和答案
• 另一个问题，这个比较栅栏和原子的问题；
• Cppmem（根据@KerrekSB 的建议）；
• Cppmem 的帮助页面；
• Spin（根据@JohnZwinck 的建议，用于分析并发系统的逻辑一致性的工具）。

（这些参考文献面向 C++11，因为这正是我接触该主题的方式。但是，据我所知，非 C++ 的答案可能是最好的，因此请随意将您的答案扩展到 C++ 之外，如您所见合身。）

你知道我是否可以在 64 位模式下运行 Cadence Incisive Formal Verifier 吗？