问题标签 [formal-methods]

有哪些代码示例可以展示KeyY的强大功能？

细节

有这么多可用的形式方法工具，我想知道 KeyY 在哪里比它的竞争对手更好，以及如何？一些可读的代码示例对比较和理解很有帮助。

更新

在 Key 网站上搜索，我找到了书中的代码示例——那里有合适的代码示例吗？

此外，我在 TimSort 中找到了一篇关于 Key 在 Java 8 的 mergeCollapse 中发现的错误的论文。什么是 TimSort 中展示 KeyY 实力的最小代码？然而，我不明白为什么模型检查不能找到错误——一个包含 64 个元素的位数组不应该太大而无法处理。其他演绎验证工具是否同样能够找到错误？

是否存在具有合适代码示例的既定验证竞赛？

这是示例：

这个例子最弱的前提是什么？

我想也许 y < 3 是一个答案。

如果没有，你能详细告诉我为什么吗？

我在进行模型验证时收到此错误，编译字符串是

自旋-a testTdma.pml

最大搜索深度太小，深度 = 9999 个状态

我不明白这个错误背后的原因。有人在使用 ISPIN 1.1.4 版和 SPIN 6.4.7 时遇到过这个吗

根据我对 TLA 的理解，最终的操作 (<>) 不允许在下一个状态下发生口吃。那么，是不是意味着下一个状态变量在无限频繁（[]<>）的情况下是不允许卡顿的呢？

以天气状况为例，无限常常可以描述为一年中最终会有很多天（我们不知道什么时候会发生）会下雨，但下雨天后天气一定是晴天？

我对无限经常的理解是正确的吗？如果我错了，请纠正我。

谢谢你。

对于最弱的前置条件和最强的后置条件，这是正确的吗？

{P} x = xx; {x'=x}
P: x = 0

{真} y = yy; {Q}
问：y = 0

编辑：

我开始应用它如下：

{true} y = y - y {Q} ==> sp(y = yy; true) = ∃x,y = xx ∧ true

现在我不知道该怎么办；在我看来，“y = 0”最有意义，但这似乎不正确。

我正在尝试对数值变量和布尔变量之间的关系进行建模，其中如果数值变量在某个范围内，则布尔变量将改变值。我是 Alloy 的新手，无法理解如何充分限制我的范围以产生明显的反例。我的代码如下：

由于o.integer是整数值并且范围从 0 到 10，因此它只能是 10 种不同选择之一。我指定每个Object应该只有一个integer和一个discrete。所以在我看来，这里实际上只有 10 个案例需要检查：每个integer. 然而，即使有 1000 个案例，我也得到了

没有找到反例。

如果我删除integer变量和相关事实，那么它几乎会立即找到反例。我也尝试过使用其他求解器并在选项中增加各种深度和内存值，但这并没有帮助，所以很明显我的代码有问题。

如何限制我的范围以使 Alloy 找到反例（通过迭代 的可能值integer）？谢谢！

我想知道是否有一种方法可以为 NuSMV 中的给定 LTL 公式生成不同的可能反例。如果我们需要为 LTL 公式生成反例，它会为我们生成一个。但是由 NuSMV 生成的那个可能不是最令人兴奋或最有见地的，因为对于相同的 LTL 公式可能还有其他反例。

你能建议一些一般的方法来让 NuSMV 产生一些与其产生的反例不同的反例吗？

一种方法是修改 LTL 公式本身，以便 NuSMV 一次性生成的反例对我们来说很有趣。但我相信系统的操纵过多，无法获得您想要的结果。

另外，您需要事先知道有趣的结果。但如果我已经知道有趣的反例，我为什么要让 NuSMV 再次向我确认呢？那么为什么还要麻烦设计一个 LTL 表达式来给出所需的反例呢？我希望 NuSMV 生成其他我没有想到的有趣的反例，从而增加价值。

如果在 NuSMV 中不可能，您能否建议任何其他可能的 LTL 模型检查器？

完全公开，这是针对大学课程的。我不希望直接得到答案，但我们将不胜感激。

我需要使用 Z 表示法对 Item 实体进行建模。这是描述：

项目：每个项目都有一个名称和一个唯一的 ID，可用于唯一地描述该项目。一个项目也有一个价格（正浮动）和一个类别。

部分要求是在没有量词的情况下对这些实体进行建模。

这是我最终得到的，但我不确定它是否正确：

项目的架构

想法是名称是字符串的某种组合，ID 是正整数和所述名称的元组，价格和类别都映射到总函数。

第一个谓词是确保价格为正，第二个谓词是确保 ID 的唯一性，即将域减少到所有尚未分配的整数。不过，我不认为这是正确的。

我试图在Coq中找到一个类似于几何中的线公理的示例公理：如果给定两个点，那么在这两个点之间存在一条线。我想看看如何在 Coq 中定义它。固有地选择这个简单的直线公理来查看非常原始的东西是如何定义的，因为我很难在自然语言之外定义它。

具体来说，我已经看到了这两个公理，并且想知道在 Coq 中如何定义这两个公理：

1. 任何两个不同的点总是确定一条线
2. 一条线的任意两个不同点唯一地确定这条线

似乎您可以将它们合并到一个定义中，所以我想从语法和语义上了解如何在 Coq 中编写它。

我真的不知道如何编写 Coq，只是想看看他们是如何做到的。但是，如果我要尝试，它似乎是这样的：

但这需要一个 Line 和一个 Point 对象。

我试图了解如何用forallRuby 或 JavaScript 等过程或 OO 语言来实现。例如（这是 Coq）：

我这样做的尝试只是定义一个诸如此类的类（调用MainAxiom == ax）。

这有各种各样的错误。它本质上是说“对于你用点 p1 和 p2 创建的每个公理，它必须满足在一条线上的属性等。”这并不完全符合我的要求。我希望它完成定义实际公理的数学目标。

想知道如何用像 Ruby 或 JavaScript 这样的语言来实现这一点，如果不能直接实现的话，就尽可能接近。即使它只是一个 DSL 或定义一些数据的对象，知道如何作为替代方案也会很有帮助。

让我印象深刻的第一部分是，attr :p1和 attr 定义似乎适用于每个实例。也就是说，它似乎说了一些关于forall的内容，但我无法确定它。

也许更像这样的东西更接近：

我只想让任何东西都接近forall过程/OO语言的定义。