程序验证之Dafny--证明霍尔逻辑的半自动化利器

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　一、What is Dafny?【来自官网介绍 Dafny 】

1)介绍

Dafny 是一种支持验证的编程语言，配备了一个静态程序验证器。

通过将复杂的自动推理与熟悉的编程习语和工具相结合，使开发者能够编写可证明正确的代码（相对于 {P}Ｓ{Q} 这种霍尔三元组的规范而言）。

Dafny 还可以将 Dafny 代码编译到熟悉的开发环境，如 C#、Java、JavaScript、Go 和 Python;使得严格的验证成为开发过程的有机组成部分，从而减少了可能在测试中被遗漏的、代价高昂的后期错误。

2)原理

Dafny验证器根据我们提供的前置条件，后置条件，以及循环不变式，自动生成验证条件（Verification Condition，VC）的逻辑公式。这些验证条件主要包含，不变式的可达性，归纳性，以及使用循环不变式证明后置条件。这些逻辑公式都会交给同样是由微软开发的SMT求解器Z3来求解，并依据求解结果，返回验证结果。

二、使用快速入门:

2.1 一个.dfy后缀的文件:

程序主要包含以下几部分：

类型(types)

方法(methods)

函数(functions)

用户自定义的类型包括类（class）和归纳数据类型(inductive class)

类class本身也包含一组声明(declarations)、介绍字段（introducing fields）、方法(methods)和函数(functions)

注释：// 双斜杠或者 /* xxxxx */

2.1.1基本定义

在类中，定义字段x为数据类型(types)T：　var x: T

注意事项：

数据类型必需手动申明的，不会被自动推断。
通过在声明前加上关键 ghost 可以将该字段声明为幽灵（即用于规范而不是执行）字段。

Dafny 的9种数据类型包括：

bool：布尔值
int：无界整数
string: 字符串
class/inductive class: 用户自定义的类和归纳类、
set<T>：不可变的无序集合
seq<T>：不可变的有序集合
array<T>、array2<T>、array3<T>: 多维数组类型
object：所有类型的超类
nat：范围是int一半，非负整数。

2.1.2方法 methods

方法的声明如下：

method M(a: A, b: B, c: C) r eturns (x: X, y: Y, z: Y)  //输入输出参数
requires Pre	//前置条件
modifies Frame  //框架
ensures Post	//后置条件
decreases TerminationMetric //变体函数
{
Body //函数体`
}

其中：

a, b, c : 输入参数
x, y, z : 输出参数
Pre: 表示方法前提条件的布尔表达式
Frame: 表示类对象的集合，可以被方法更新(Frame denotes a set of objects whose fields may be updated by the method)
Post: 是方法后置条件的布尔表达式
TerminationMetric: 是方法的变体函数(TerminationMetric is the method’s variant function)
Body: 是实现方法的语句。

2.1.2.1框架Frame

框架Frame 是单个或多个对象组成的表达式的集合。(见下面例子)

框架Frame是由类内对象和类外方法内对象两部分组成。(反正就是一堆类对象的集合）

例如，如果 c 和 d 是类C的对象，那么以下每行意思是一样的。

modifies {c, d}

modifies {c} + {d}

modifies c, {d}

modifies c, d

如果方法内啥都没写，那么前置和后置条件默认为真，框架默认为空集。

2.1.2.2变体函数 variant function

变体函数是一个表达式组成的列表，表示由给定表达式组成的字典元组，后跟隐含的“top”元素。

如果省略没写的话，Dafny 将猜测该方法的变体函数，通常是以该方法的参数列表开头的字典元组。

Dafny IDE 将在工具提示中显示猜测。

2.1.2.3ghost 关键字

通过在声明之前加上关键字 ghost 可以将方法声明为 ghost方法（仅规范而不用于执行）。

2.1.2.4this 关键字

默认情况下，类中的方法都具有隐式接收器参数 this。可以通过在方法声明之前使用关键字 static 来删除此参数。

类 C 中的静态方法 M 可以由 C.M(...) 调用。

2.1.2.5构造函数/构造体 constructor

在类中，一个方法可以通过将method关键字替换为constructor，申明一个构造方法。

构造函数(构造方法)只能在分配对象时调用（参见示例）

对于包含一个或多个构造函数的类，对象创建必须与对构造函数的调用一起完成。

通常，一个方法当然得有一个名字，但是一个类可以有一个没有名字的构造函数，也就是匿名构造函数 constructor (n:int )

constructor (n: int) //constructor 匿名构造器` 
modifies this //框架内对象的构造体 this就是this.frame？`

{
  Body
}

2.1.3函数 function

函数具有以下形式：

function F(a: A, b: B, c: C): T
requires Pre  //前置条件pre
reads Frame	//框架frame
ensures Post //后置条件post
decreases TerminationMetric //变体函数
{
  Body	//函数体
}

a, b, c : 输入的形参，
T : 返回结果的类型，
Pre: 表示函数前提条件的布尔表达式，
Frame: 函数体body需要的对象列表
Post: 函数的后置条件布尔表达式
TerminationMetric: 变体函数
Body: 定义函数的表达式。

前置条件允许函数是部分的(只用前置就行不用写后置），即前置条件表示函数何时定义，并且 Dafny 会验证函数的每次使用都满足前置条件。

通常不需要后置条件，因为函数在函数体内已经给出了完整的定义。

例如：

（写个后置加个保险也行，一般后置就是声明该函数的基本属性，比如Factorial这个函数所有数字都≥1）

function Factorial(n: int): int
requires 0 <= n //前置条件pre
ensures 1 <= Factorial(n) //后置条件post
{
 if n == 0 then 1 else Factorial(n-1) * n //函数体body
}

要在后置条件中引用函数的结果，请使用函数本身的名称，如示例中所示。

默认情况下，函数是ghost，不能从可执行（非ghost）代码中调用。

为了使它从ghost变成非ghost，用关键字function method替换 function.

一个返回布尔值的函数可以用关键字声明，然后省略冒号和返回类型。

如果函数或方法被声明为类class成员，则它具有隐式接收器参数 this。可以通过在声明之前加上关键字static来删除此参数。

类 C 中的静态函数 F 可以被 C.F(...) 调用。

E.g.2:[educoder实训实例]:

method test(n: int) returns (sum: int)
  requires n >= 0
  ensures sum * 2 == n * (n+1)
{
  sum := 0;
  var i:int := 0;
  while i <= n
  invariant i<=n+1
  invariant sum*2 == i*(i-1)

  {
    sum := sum + i;
    i := i + 1;
  }
}

2.1.3.1 类 class

一个类定义如下：

class C {
 // member declarations go here
}

其中类的成员（字段、方法和函数）在花括号内定义（如上所述）。

2.1.3.2数据类型 datatypes

归纳数据类型（inductive datatype）是一种类型，其值是用一组固定的构造函数创建的。

数据类型为Tree带有构造函数 Leaf 和 Node 的函数声明如下：

datatype Tree = Leaf | Node(Tree, int, Tree)//Leaf为无参构造函数 Node为有参

构造函数由竖线分隔。无参数构造函数不需要使用括号，如 Leaf 所示。

对于每个构造函数 Ct，数据类型隐式声明了一个布尔成员 Ct?，对于已经使用 Ct 构造函数赋的值的成员，它返回 true。例如，在代码片段之后：

var t0 := Leaf; var t1 := Node(t0, 5, t0);

表达式 t1.Node结果为 true, t0.Node结果为false。

如果两个数据类型值是使用相同的构造函数和该构造函数的相同参数创建的，则它们是相等的。因此，对于像 Leaf、t.Leaf 这样的无参数构造函数，Dafny会给出与 t == Leaf 相同的结果。(没看懂，不管了)

构造函数可以选择为其任何参数声明析构函数，这是通过为参数引入名称来完成的。例如，如果 Tree 被声明为：

datatype Tree = Leaf | Node(left: Tree, data: int, right: Tree)

那么t1.data == 5和t1.left == t0在上面的代码片段之后保持不变。(还是没懂)

2.1.3.3泛型 Generics

Dafny同其他语言一样都有泛型，任何类、方法、函数都可以有类型参数，在<>中申明该数据类型T

class MyMultiset<T> {
 /*...*/
}		//类泛型
datatype Tree<T> = Leaf | Node(Tree<T>, T, Tree<T>) //自定义数据泛型
method Find<T>(key: T, collection: Tree<T>) { //方法泛型`
 /*...*/
}

function IfThenElse<T>(b: bool, x: T, y: T): T {	//函数泛型
 /*...*/
}

2.1.3.4声明 Statement

以下是 Dafny 中最常见语句:

var LocalVariables := ExprList;
Lvalues := ExprList;
assert BoolExpr;
print ExprList;

if BoolExpr0 {
  Stmts0
} else if BoolExpr1 {
  Stmts1
} else {
  Stmts2
}

  while BoolExpr
  invariant Inv
  modifies Frame
  decreases Rank
{
  Stmts
}
 match Expr {
  case Empty => Stmts0
  case Node(l, d, r) => Stmts1
}
 break;
 return;

函数/方法的返回值赋值给变量

(就是将函数/方法返回的值或对象赋给一个局部变量而已） var LocalVariables := ExprList; var 语句引入了局部变量。 Lvalues := ExprList;

赋值语句将 ExprList变量赋给Lvalues。这些分配是并行执行的（更重要的是，所有必要的读取都发生在写入之前），因此左侧必须表示不同的 L 值。每个右侧都可以是以下形式之一的表达式或对象创建：

new T

new T.Init(ExprList)

new T(ExprList)

new T[SizeExpr]

new T[SizeExpr0, SizeExpr1]

第一种形式分配一个类型为 T 的对象。

第二种形式另外在新分配的对象上调用初始化方法或构造函数。

第三种形式是当调用匿名构造函数时的语法。

其他形式分别了T是一维和二维数组对象的匿名构造方法

assert 声明

assert 语句判断后面的表达式结果是否为真（由验证器验证）。

print 打印语句

打印语句将给定打印表达式的值输出到标准输出。字符串中的字符可以转义；例如，对 print 语句感兴趣的是 \n 表示字符串中的换行符。

if 选择语句

if 语句是通常的语句。该示例显示了使用 else if 将备选方案串在一起。像往常一样，else 分支是可选的。

while 循环语句

while 语句是通常的循环，其中
invariant 声明给出了一个循环变量
modifies语句限制了循环的框架
reduction语句从循环中引入了一个变体函数。

默认情况下，循环不变式为真，修改框与封闭上下文中的相同（通常是封闭方法的修改子句），并从循环保护中猜测变体函数。(真没看懂）

while BoolExpr //布尔表达式-循环条件`
  invariant Inv
  modifies Frame
  decreases Rank

{
  Statements
}

break语句

break 语句可用于退出循环，而 return 语句可用于退出方法。

2.1.4 表达式 Expressions

Dafny 中的表达式与类 Java 语言中的表达式非常相似。以下是一些值得注意的差异。

2.1.4.1基本运算符

除了短路布尔运算符 && (and) 和 || （或），Dafny 有一个短路蕴涵运算符 ==> 和一个 if-and-only-if 运算符 <==>。

正如它们的宽度所暗示的那样，<==> 具有比 ==>低的绑定力，而后者又比 && 和 ||具有更低的绑定力。

Dafny 比较表达式可以是链式的，这意味着相同方向的比较可以串在一起。例如，

0 <= i < j <= a.Length == N

含义相同：

0 <= i && i < j && j <= a.Length && a.Length == N

请注意，布尔相等可以使用 == 和 <==> 来表示。这些之间有两个区别。首先，== 比 <==> 具有更高的约束力。其次，== 是链接，而 <==> 是关联的。也就是说，a == b == c 与 a == b && b == c 相同，而 a <==> b <==> c 与 a <==> (b <== > c)，这也与 (a <==> b) <==> c 相同。

整数运算

对整数的运算是常用的运算，除了 /（整数除法）和 %（整数模）遵循欧几里德定义，这意味着 % 总是导致非负数。（因此，当 / 或 % 的第一个参数为负数时，结果与您在 C、Java 或 C# 中得到的结果不同，请参阅 http://en.wikipedia.org/wiki/Modulo_operation。）

集合运算

集合上的操作包括+（并）、*（交）和-（集合差）、集合比较运算符<（真子集）、<=（子集）、它们的对偶> 和>=，以及!! （脱节）。 S 中的表达式 x 表示 x 是集合 S 的成员，而 x !in S 是一个方便的写法 !(x in S)。

要从某些元素创建一个集合，请将它们括在花括号中。例如，{x,y} 是由 x 和 y 组成的集合（如果 x == y，则为单例集），{x} 是包含 x 的单例集，{} 是空集。

序列运算

对序列的操作包括 +（连接）和比较运算符 <（适当的前缀）和 <=（前缀）。成员资格可以像集合一样检查：x in S 和 x !in S。序列 S 的长度表示为 |S|，并且此类序列的元素具有从 0 到小于 |S| 的索引。表达式 S[j] 表示序列 S 的索引 j 处的元素。表达式 S[m..n]，其中 0 <= m <= n <= |S|，返回一个序列，其元素是S 从索引 m 开始（即，从 S[m]、S[m+1]、……直到但不包括 S[n]）。表达式 S[m..]; （通常称为“drop m”)与 S[m..|S|] 相同；也就是说，它返回除 S 的前 m 个元素之外的所有元素的序列。表达式 S[..n] ; （通常称为“take n”）与 S[0..n] 相同，即它返回由 S 的前 n 个元素组成的序列。

如果 j 是序列 S 的有效索引，则表达式 S[j := x];是类似于 S 的序列，只是它在索引 j 处有 x。

最后，要从一些元素组成一个序列，请将它们括在方括号中。例如，[x,y] 是由两个元素 x 和 y 组成的序列，使得 [x,y][0] == x 和 [x,y][1] == y，[x] 是唯一元素是 x 的单例序列，[] 是空序列。