jro*_*sch 25
每个工具都有独特的设计,由具有不同目标和理念的不同人构建和影响,但作者都是朋友,并且已经在彼此的几个办公室中待了很多年.
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*最近获得了使用受精益战术语言影响很大的战术的能力.
F*对Dafny和其他改进类型等工具的主要创新是使用Dijkstra Monads来描述代码的"效果",使效果设计师能够控制生成的验证条件.DM允许用户在不同级别进行推理,例如Pure效果中的代码不能使用状态,或抛出异常,用户可以忽略他们不使用的有效功能.
Lean的设计受Coq和其他内涵类型理论的影响很大,并且与它们更相似,Lean的目标是通过将自动化(SMT)世界的技术引入类型理论来结合最好的自动化和交互式定理证明.世界.它具有非常强大的元编程能力,并且已经获得越来越多的自动化.Lean不需要SMT求解器,并以专门的方式为Lean的类型理论重新实现许多核心过程.
您可以将F*和Lean视为覆盖类似空间,但强调不同的到达方式.
如果不澄清,我很乐意详细说明.
资料来源:Lean的核心开发人员,F*的开发人员,有时也是Dafny的用户和贡献者,在MSR工作了大约7个月,亲自了解所有工具作者.
| 归档时间： |
|
| 查看次数： |
1460 次 |
| 最近记录： |