0

<编辑> 关于这个问题离题且过于基于意见，我会尽量说得更清楚。我的目标是不知道是否存在这样的工具，我对关于什么是最好的工具的意见不感兴趣。在我写这个问题的时候，我花了很多时间在互联网上搜索，发现只是旧的死项目，但是存在这样的 Java 工具，我不敢相信 C# 没有任何东西。我认为这个问题与编程（代码验证）有关，并不是真的在征求意见。此外，要找到这些信息仍然不容易，我认为我的回答可以帮助节省某人的时间。也就是说，我不是 stackoverflow 的专家，如果您仍然认为问题/答案不适合该网站，请随时删除它。< /编辑>

我找到了 Moonwalker http://fmt.cs.utwente.nl/tools/moonwalker/，但最后一次更新是在 2009 年完成的，我认为它不支持 .net4.5（而且文档记录很差）。

这个问题的答案建议将 CodeContracts 作为模型检查工具模型检查工具 c#，但我已经尝试使用它，但我认为它并不是一个模型检查器，与 Java Path Finder for Java 的方式不同。我穿了吗？可以像 JPF 一样使用吗？

我需要能够知道代码的某个部分是否以可能死锁的方式设计。假设这是学校的事情，即使我确定我的代码正在运行，我也必须对它进行模型检查。（是的，我们被允许并鼓励在互联网上查看）。

4

2 回答 2

0

正如用户@HighCore 所说，经过大量搜索后，我可以说不存在像我描述的那样成熟且最新的工具。

于 2013-09-04T12:42:28.717 回答
0

模型检查通常是指显式方法，但是符号方法同样先进，并且可以说更有能力建立实际代码的属性。

对于图灵完备的语言，验证问题是不可判定的，因此模型检查工具通常接受功能较弱的语言作为输入。这意味着在检查之前必须将您的问题转换为该语言。这就是为什么您没有遇到任何“C# 模型检查工具”的原因。

你看过Boogie和类似 C# 的Dafny吗？这些（基本上）用于使用Hoare logic进行注释。

或者，您可以考虑在（手动）将 C# 解决方案转换为Promela之后对它进行模型检查，然后使用SPIN。

相关工具（例如 C-to-Promela 翻译器）在此处列出。

于 2013-10-10T09:26:33.020 回答