lean，f *和dafny有什么区别？

作者: 狗头军师
发布时间: 2024-12-28 02:31:40 (17天前)

2 条回复

1#
回复此人
v-star*위위 | 2020-08-19 15-52

每个工具都有独特的设计，并且由具有不同目标和理念的不同人构建和影响，但是作者都是朋友，并且在彼此的几个办公室坐了很多年。 Rustan Leino设计了Dafny作为他所构建的许多系统（包括ESC Java和Spec＃）的继承者。 Dafny基于Java或C＃这样的命令式语言，能够编写Hoare逻辑样式状态不变式，这使语言的用户可以验证有关方法以及使用可变状态，循环，数组等的对象的属性。达夫尼（Dafny）的核心理论是主要由Rustan和少数合作者设计的自定义程序逻辑。Dafny通过将其生成的验证条件编译为Boogie中间验证语言来释放验证条件，然后将它们编译成查询，然后将查询传递给SMT求解器（例如Z3或CVC4）以进行放电。 Dafny的设计目标是使用户感到非常类似于命令式面向对象的语言，他们熟悉验证程序的附加功能。 F *是基于Nikhil Swamy和合作者设计的一种新型理论，它最初是一种类似于ML的编程语言，并加入了以Dafny风格出现的细化类型，但由于近年来的发展，外部的众多补充，以及来自Dafny，Lean，LiquidHaskell等的影响。 F *也将其验证条件转换为SMT求解器（例如Dafny），但不使用中间验证语言（例如Boogie）。F *最近获得了使用受精益战术语言严重影响的战术的能力。 F *对诸如Dafny和其他优化类型之类的工具的主要创新是使用Dijkstra Monads来描述代码“效果”的一种方式，使效果设计者可以控制所生成的验证条件。DM允许用户在不同级别进行推理，例如，Pure效果中的代码无法使用状态或引发异常，并且用户能够忽略他们未使用的有效功能。精益的设计在很大程度上受Coq和其他内涵类型理论的影响，并且与它们非常相似，精益的目标是通过将自动化（SMT）世界中的技术引入类型理论，以结合最佳的自动化和交互式定理证明世界。它具有非常强大的元编程能力，并且已经获得越来越多的自动化。精益不需要SMT求解器，并且可以以精益类型理论的专用方式重新实现许多核心过程。您可以将F *和Lean视为覆盖相似的空间，但要强调到达那里的不同方法。如果无法澄清，我很乐意详细说明。资料来源：Lean的核心开发人员，F *的开发人员以及Dafny的用户和贡献者，曾在MSR工作了大约7个月，并亲自认识了所有工具作者。

编辑

登录后才能参与评论