是否有用于 C# 的模型检查软件（如 Java Path Finder）？ [关闭]答案

【问题标题】：Is there a Model Checking software (like Java Path Finder) but for C#? [closed]是否有用于 C# 的模型检查软件（如 Java Path Finder）？ [关闭]
【发布时间】：2013-09-03 19:37:56
【问题描述】：

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

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

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

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

【问题讨论】：

我认为 .Net 没有类似的东西。这并不是真正需要的，因为 .Net 代码简短、美观且功能强大。它没有处理语言限制的复杂技巧，例如没有Events 和Delegates。由于Async / await，线程、并行和异步在C# 5 中非常漂亮，它允许在单个Try/Catch 中控制多个异步调用。

标签： c# .net-4.5 model-checking jpf

【解决方案1】：

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

【讨论】：

【解决方案2】：

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

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

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

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

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

【讨论】：