介绍

Dafny 是一种旨在使编写正确代码变得容易的语言。怎么更容意的验证正确性呢？Dafny依靠高级注释来实现。通过高级注释（high-level annotations）的推理和验证，一段代码的逻辑可以用高级注释更自然抽象的表达出来，当然这样更加容易编写和验证，且不易写错。

编译dafny程序后，dafny会生成与高级注释匹配的逻辑证明，来告诉程序员这个程序逻辑正不正确，错了也会有报错。Dafny这样实际上是把编写无错误代码减轻为编写无错误注释，这样写起来当然更容易，因为注释更短更直接。下面举个例子：

forall k: int :: 0 <= k < a.Length ==> 0 < a[k]

这个例子是说：对于所有数组下标索引k，其索引对应的数组值a[k]>0。通过编写这段注释，可以验证这个是正确的。

除了证明程序员写的高级注释是否正确外，Dafny还能实时验证逻辑。它能边写程序边验证，比如数组越界、空引用、除以零等，还可以证明循环中代码是否终止，总之功能非常强大。

那么在何处编写Dafny呢？可以上github下载Dafny语言包，用命令行打开Dafny.exe文件输入程序就可以验证，也可以在浏览器web上打开rise4fun网站，这网站上能实时编写并且有教程。如果想有更好的体验比如高亮注释实时报错这种功能的话，可以用VScode下载相应 适用广泛的基础单选

markdown content