他们来自微软，看起来像是证明助手？除了语法上的差异之外，它们在实践中是否有使它们不同的方面（比如能力自动化、表达能力等）？我对形式验证很新。
编辑：我不是要求哪个更好，只是对这些工具提供的不同特性进行技术比较感兴趣。我正在寻找类似这个的东西。
1个回答
47
每个工具都有独特的设计，并由不同的人以不同的目标和哲学构建和影响，但作者们都是朋友，多年来一直坐在彼此几个办公室内。Rustan Leino将Dafny设计为他之前构建的许多系统（包括ESC Java和Spec＃）的继承者。
Dafny基于类似于Java或C#的命令式语言，具有编写Hoare逻辑风格状态不变量的能力，这使得语言的用户可以验证关于使用可变状态、循环、数组等方法和对象属性的特性。 Dafny的核心理论是由Rustan和一些合作者大多数自定义的程序逻辑。 Dafny通过将其生成的验证条件编译成Boogie中间验证语言来解除它所生成的验证条件，然后将其编译成查询，这些查询传递给像Z3或CVC4这样的SMT求解器来释放。
Dafny的设计目标是感觉非常类似于用户熟悉的命令式面向对象语言，增加了验证程序的功能。
F*基于Nikhil Swamy和合作者设计的新类型理论，它始于类似ML的编程语言，添加了Dafny风格的细化类型，但由于众多外部添加以及对Dafny、Lean、LiquidHaskell等的影响而在过去几年中发生了很大变化。
F*也将其验证条件转换为像Dafny这样的SMT求解器，但不使用类似于Boogie的中间验证语言。F*最近获得了使用受Lean策略语言影响的策略的能力。
与Dafny和其他细化类型工具相比，F*的主要创新是使用Dijkstra Monads来描述代码的“效果”，使效果设计者控制所生成的验证条件。DM允许用户在不同级别进行推理，例如，在“Pure”效果中的代码不能使用状态或抛出异常，用户能够忽略他们不使用的有副作用的特征。Lean 的设计受到 Coq 和其他内涵类型理论的影响很大，它与它们非常相似。Lean 的目标是将自动化和交互式定理证明器的优点结合起来，通过将自动化（SMT）领域的技术引入类型理论领域来实现这一目标。它具有非常强大的元编程能力，并且越来越多地实现了自动化。Lean 不需要 SMT 求解器，并以专门的方式重新实现了许多核心过程以适应 Lean 的类型理论。
您可以将 F* 和 Lean 视为覆盖相似空间但强调不同到达方式的工具。
如果这还不清楚，我很乐意进一步阐述。
来源：Lean 核心开发人员、F* 开发人员，有时使用并贡献于 Dafny，并在 MSR 工作了约 7 个月，认识所有工具作者。
Dafny的设计目标是感觉非常类似于用户熟悉的命令式面向对象语言，增加了验证程序的功能。
F*基于Nikhil Swamy和合作者设计的新类型理论，它始于类似ML的编程语言，添加了Dafny风格的细化类型，但由于众多外部添加以及对Dafny、Lean、LiquidHaskell等的影响而在过去几年中发生了很大变化。
F*也将其验证条件转换为像Dafny这样的SMT求解器，但不使用类似于Boogie的中间验证语言。F*最近获得了使用受Lean策略语言影响的策略的能力。
与Dafny和其他细化类型工具相比，F*的主要创新是使用Dijkstra Monads来描述代码的“效果”，使效果设计者控制所生成的验证条件。DM允许用户在不同级别进行推理，例如，在“Pure”效果中的代码不能使用状态或抛出异常，用户能够忽略他们不使用的有副作用的特征。Lean 的设计受到 Coq 和其他内涵类型理论的影响很大，它与它们非常相似。Lean 的目标是将自动化和交互式定理证明器的优点结合起来，通过将自动化（SMT）领域的技术引入类型理论领域来实现这一目标。它具有非常强大的元编程能力，并且越来越多地实现了自动化。Lean 不需要 SMT 求解器，并以专门的方式重新实现了许多核心过程以适应 Lean 的类型理论。
您可以将 F* 和 Lean 视为覆盖相似空间但强调不同到达方式的工具。
如果这还不清楚，我很乐意进一步阐述。
来源：Lean 核心开发人员、F* 开发人员，有时使用并贡献于 Dafny，并在 MSR 工作了约 7 个月，认识所有工具作者。
- jroesch
3
F和Dafny鼓励不同的编程模式，Dafny优化了Java风格代码的编写和推理，而F则专为ML风格代码的编写和推理提供灵活性，并提供了推理模型。通常，某些数据结构在一种语言中很容易编写，但在另一种语言中却不是这样。在这种情况下，隐式Hoare推理可能更有帮助，而不是效果单子。 - jroesch
这是一个很棒的总结。谢谢@jroesch！ - sligocki
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接