问题标签 [formal-methods]

我记得不久前读过一些关于 C 的正式规范语言的内容，但现在我需要它却找不到它。

它受到 JML 的启发，就我所见使用相同的语法。

我发现它的唯一参考是一篇论文，但我所说的比这更精致。

如果这给你敲响了警钟……

如果没有人知道这一点，我会很高兴听到一种在 C 中进行形式验证和自动测试生成的方法。

提前致谢。

我正在研究自动化软件验证的要求，即一个接收代码的程序（用 C 和 Java 等语言编写的普通程序代码），生成一堆定理，说每个循环必须最终停止​​，不会违反任何断言，将永远不会取消引用空指针等，然后将其传递给定理证明者以证明它们实际上是正确的（或者在代码中找到指示错误的反例）。

问题是使用什么样的逻辑。两个主要职位似乎是：

1. 一阶逻辑就好了。

2. 一阶逻辑不够表达，需要高阶逻辑。

问题是，这两个职位似乎都有很多支持。那么哪一个是对的呢？如果是第二个，是否有任何您想做的事情的可用示例，基于一阶逻辑的验证器有问题？

我被困在这个正式的方法作业问题上，我不确定我做错了什么。

我有两个签名，Item 和 ToDo，它们的定义如下：

我必须定义一个函数，它将具有给定日期和类别的项目插入到待办事项列表集中。诀窍是列表集应该按项目的到期日期排序。步骤和日期都有排序。

我的问题是：如何在 ToDo.list 中获取具有特定日期的项目集？我有这个功能：

我尝试使用以下代码（及其变体）来获取项目集：

这不起作用，我理解为什么，因为 t.due.st 留下了一组日期。然而，从那时起的其他尝试并没有让我到达那里。在到达 t 之前，我尝试使用括号来评估“due.st”和“d”之间的连接，但这不起作用，我尝试使用方括号来更改顺序，但是不起作用。我知道我在这里做错了什么，但我不知道是什么。

从以下想法继续：是否有任何可证明的现实世界语言？

我不了解你，但我厌倦了编写我无法保证的代码。

在问了上述问题并得到了惊人的回应（谢谢大家！）之后，我决定缩小对Haskell的可证明的、实用的方法的搜索范围。我选择 Haskell 是因为它实际上很有用（为它编写了许多 Web 框架，这似乎是一个很好的基准），而且我认为它在功能上足够严格，可以证明，或者至少允许测试不变量。

这就是我想要的（但一直找不到）

我想要一个可以查看 Haskell 函数的框架，添加，用伪代码编写：

- 并检查某些不变量是否适用于每个执行状态。我更喜欢一些正式的证明，但是我会满足于模型检查器之类的东西。
在此示例中，不变的是给定值a和b，返回值始终是总和a+b。

这是一个简单的例子，但我不认为这样的框架不可能存在。可以测试的函数的复杂性肯定会有一个上限（一个函数的 10 个字符串输入肯定会花费很长时间！）但这会鼓励对函数进行更仔细的设计，并且与使用其他形式的函数没有什么不同方法。想象一下使用 Z 或 B，当您定义变量/集合时，您要确保为变量提供尽可能小的范围。如果您的 INT 永远不会超过 100，请确保将其初始化！像这样的技术和适当的问题分解应该——我认为——允许对像 Haskell 这样的纯函数式语言进行令人满意的检查。

我对形式化方法或 Haskell 的经验还不是很丰富。让我知道我的想法是否合理，或者您认为 haskell 不适合？如果您建议使用不同的语言，请确保它通过了“has-a-web-framework”测试，并阅读原始问题:-)

是否有工具可以处理模型检查大型、真实世界、主要是 C++ 分布式系统，例如 KDE？

（KDE 在使用 IPC 的意义上是一个分布式系统，尽管通常所有进程都在同一台机器上。是的，顺便说一句，这是“分布式系统”的有效用法 - 检查 Wikipedia。）

该工具需要能够处理进程内事件和进程间消息。

（假设如果该工具支持 C++，但不支持 KDE 使用的其他东西，例如 moc，我们可以一起破解一些东西来解决这个问题。）

我很乐意接受不太通用的（例如，专门用于查找特定类别错误的静态分析器）或更通用的静态分析替代方案，以代替实际的模型检查器。但我只对能够实际处理 KDE 规模和复杂性项目的工具感兴趣。

我试图（经典地）证明

在考克。我想要做的是相反地证明它：

我的问题是第 (2) 和 (5) 行。我不知道如何选择 U 的任意元素，证明一些关于它的东西，并得出结论。

有什么建议（我不致力于使用对立）？

我正在尝试使用 Function 使用度量来定义递归定义，但出现错误：

我在底部发布了整个源代码，但我的功能是

我知道问题出在 foralls 上：如果我用 True 替换它们，它就可以工作。我也知道如果我的右手边使用含义（->），我会得到同样的错误。Fixpoint 适用于 foralls，但不允许我定义度量。

有什么建议吗？

正如所承诺的，我的完整代码是：

所以我在Alloy中有以下代码：

但这不会产生任何包含队列的实例，我想知道为什么。它只显示带有节点的实例。我试过等效的谓词

但输出是一样的。

我错过了什么吗？

我想将alloy4 用于自动化测试用例生成研究项目。谁能帮我解决这个问题？如何使用合金生成的实例来创建 java 实例对象？

我在一篇关于形式方法的论文中遇到了“必须折叠循环以确保终止”（准确地说是抽象解释）。我很清楚终止的含义，但我不知道折叠循环是什么，也不知道如何在循环上执行折叠。

有人可以向我解释一下折叠环是什么吗？如果它不是隐含在折叠循环的定义中，或者没有立即遵循，这如何确保终止？

谢谢