他们来自微软,看起来像是证明助手?除了语法上的差异之外,它们在实践中是否有使它们不同的方面(比如能力自动化、表达能力等)?我对形式验证很新。 编辑:我不是要求哪个更好,只是对这些工具提供的不同特性进行技术比较感兴趣。我正在寻找类似这个的东西。
每个工具都有独特的设计,并由不同的人以不同的目标和哲学构建和影响,但作者们都是朋友,多年来一直坐在彼此几个办公室内。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 个月,认识所有工具作者。