Dafny笔记

Abstract

Dafny是一种使编写正确代码变得更容易的语言。这里的正确性意味着没有运行错误,并且实际执行了程序员打算执行的操作。为了实现这一目标,Dafny依靠高级注释(annotation)来推理证明代码的正确性。一段代码的效果可以使用高级表达式抽象地描述,这更简单并且更不容易出错。Dafny将编写无错误代码的责任转移到编写无错误注释的代码上例如,Dafny中的以下注释片段表示数组的每个元素都是正的:

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

这表示对于作为数组索引的所有整数k,该索引处的值大于零。编写注释的可以帮助理解代码在更深层次上所做的事情。

Method

方法(method)是任何Dafny程序的基本单位之一,其基本使用方式如下:

method Abs(x:int) returns(y:int) //可以有多个返回值
{
    if x < 0
    {return -x;} // 注意分支部分只有一条语句也要用{}
    else
    {return x;}
}

method 的参数和返回值可以有多个

method MutipleReturns(x:int,y:int) returns (more:int,less:int)
{
    more := x + y;
    less := x - y;
}

正如上边程序所看到的一样,method主体可以有各种语句,赋值用":="表示,多条语句之间使用分号隔开。

Dafny的真正能力是来自于注释method来指定其性质。例如使用Abs方法时我们可以预测的一个性质是,无论输入的结果如何,结果一定大于等于零,通过注释,我们可以让Dafny证明该方法的性质是否成立,从而证明程序是否符合预期。

添加注释的最基本的,最常见的方法是通过前后置条件。

前置条件通过关键字requires声明,后置条件通过关键字ensures声明。

我们看下一个例子

method Abs(x:int) returns (y:int)
ensures y >= 0
{
    if x < 0
    {return -x;}
    else
    {return x;}
}

给method的返回值取名字是为了方便后置条件的表示

就可以有多个前后置条件,不同的条件可以分开写,也可以使用"&&"连接

例如:

method MutipleReturns(x:int,y:int) returns (more:int,less:int)
    ensures less < x;
    ensures more > x;
//可以直接写成这个样子 ensures x > less && x < more
//也可以这样写 less < x < more
{
    more := x + y;
    less := x - y;
}

注意这上边的这段程序有问题,Dafny会报告后置条件不成立,因为当y为负数或零时, less >= x 。所以要对后置输入条件的y进行前置条件的限制,即满足 y 是非负数

下边是正确的代码:

method MutipleReturns(x:int,y:int) returns (more:int,less:int)
    requires y > 0
    ensures less < x < more
{
    more := x + y;
    less := x - y;
}

Function

function 返回值只需要给出类型而不需要变量名称。同样的求绝对值的函数可以这样表示

function Abs(x:int):int
{
    if x < 0 then -x
    else x
}

这声明了一个函数,它接受一个整数,并返回一个整数,与上边method不同,function的主体必须具有相同类型的表达式,这里使用了if表达式,相当于三目运算符。并且像个分支的返回值必须与函数声明中的类型相同。function的强大在于可以直接用于规范之中,例如这样

function Abs(x:int):int
{
    if x < 0 then -x
    else x
}
method m()
{
    assert Abs(-1)==1
}

除了语法的不同,还有其他部分的不同,Dafny在考虑method和function的时候会忘记method的主体,不会忘记function的主体,也就是说,Dafny不在乎method的内部到底是指什么,举个例子。

method Abs(x:int) returns (y:int)
ensures y >= 0
{
    if x < 0
    {return -x;}
    else
    {return x;}
}
method Testing()
{
    var v := Abs(-3);
    assert v >= 0; // 编译通过
    assert v == 3; //编译通不过
}

解释: Dafny 对于Abs的方法只知道后置条件所描述的性质,并不知道具体的返回值,因为程序并没有真正的执行,如果Abs是function,则两个断言都成立。

为了使上边的程序能够运行成功,我们需要给method加上更强的后置条件

method Abs(x:int) returns (y:int)
ensures y >= 0;
ensures x >= 0 ==> x == y;
ensures x < 0 ==> y == -x;
{
    if x < 0
    {return -x;}
    else 
    {return x;}
}
method Testing()
{
    var v := Abs(-3);
    assert v >= 0;
    assert v == 3;
    // 都可以通过编译
}

function 不是最终编译程序的一部分,它只是帮忙验证代码的工具。function只能在注释(前后置条件,循环不变式,断言等)中被调用,可以用它写一些递归的调用。 比如计算斐波那契数列:

function Fib(n:nat):nat
{
    if n == 0 then 0 else
    if n == 1 then 1 else
    Fib(n-1)+Fib(n-2)
}

Loop Invariants

在Dafny中,循环不变式用关键字 invariant标识,循环不变式是一个表达式,它在进入一个循环时以及循环体的每次执行都有效,它捕捉了循环的每一步都是不变的,即不管循环进行到哪一步都不会改变。像前置条件和后置条件一样,不变量是为每次循环执行保留的属性,用布尔表达式表示,例如: 下边这个例子

method m(n:nat)
{
    var i := 0;
    while i < n
    invariant i >= 0
    {
        i := i + 1;
    }
}

在这段代码中,i一开始就是非负的,那么它在每次的循环之后都能保持非负数,所以就可以讲它当作不变量加入到循环中。

Dafny只能通过分析循环不变量和循环条件来了解循环的属性,在上边的这个循环中,最后退出循环的时候是i等于n,通过添加断言可以判断Dafny是否证明了这一点

method m(n:nat)
{
    var i:= 0;
    while i < n;
    invariant i >= 0
    {
        i := i + 1;
    }
    assert i == n;
}

此时Dafny会提示断言不成立,因为它只知道循环借宿和时 i>=n 并且 i>=0

不足以证明断言成立,所以我们需要修改循环不变式,限制它超过n的可能性,可以将循环不变式改为:

invariant 0 <= i <= n

Quantifiers

Dafny中的量词采用forall的表达式,这叫做全称量词,用来表示任意的

比如我们可以下一个断言:

assert forall k :: k < k + 1

这个断言的意思就是,对于所有的k,k都小于k+1。这是恒成立的

量词为集合中的每个元素加入一个临时的名称,称为绑定变量,即上例中的k, 绑定变量的类型通常是由Dafny自动推断出来的,大多数情况下是int,量词通常用于量化数组中的所有元素,如对数组中的元素:

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

这表示数组中的所有元素都大于0 , k的范围限制确保了数组下标没有越界。

predicate

predicate是一个返回值为bool的函数,例如可以将整数数组排序定义为西边的函数

predicate sorted(a:array<int>)
    requires a != null
{
    forall j,k :: 0 <= j < l < a.Length ==> a[j] <= a[k]
}

上边程序还是会报错,因为需要访问数组,所以给这段代码需要加上可读的权限

predicate sorted(a:array<int>)
    requires a != null
    reads a
    {
        forall j,k :: 0 <= j < k < a.Length ==> a[j] < a[k]
    }

函数或者是predicate的可读范围是允许函数读取的所有存取位置,是为了保护内存,确保未在可读范围内的内存没有被修改, reads注释不是一个bool表达式,它可以随着前后置条件出现在任何位置,它指定了该函数访问的存储器的位置。Dafny会检查你没有读取未在可读范围中声明的内存。

Termination

Dafny证明所有程序都终止,有两种潜在的非终止的行为: 循环和递归函数 Dafny采用单一的方法处理这种情况,使用 decreases 注释。

decreases 注释指定一个值,称为 终止度量,每次遍历循环或调用递归的时候,这个值都将严格地缩小。此值有界,因此它不能永远减少,这样这个值从任意有限值开始,循环或递归必须停止,Dafny 证明了在每次迭代时,终止度量都变小了。

Dafny可以在使用 decreases 时使用多种值,但是最常见的是整数,整数有个自然下限,零,通常很容易证明他们减少,例如下边的这个代码。

var i,n := 0,11;
while i < n
decreases n - i
{
    i := i + 1;
}

Set

集合类型是Dafny验证的核心工具之一,集合在Dafny是无序的,不可重复的,通常集合可以是任何数据类型,包括对象。具体性质看下边代码

var s := {}; empty set
var s2 := {1,2,3};
assert s2 == {1,2,1,2,3,3};
var s3,s4 := {1,2},{1,4};

assert s2 + s4 == {1,2,3,4} //∪
assert s2 * s3 == {1,2} && s2 * s4 == {1}; //∩
assert s2 - s3 == {3}; //差

另外,集合还支持比较运算符,例如:

Exercise

  • 验证顺序查找的正确性
method Find(a:array<int>,key:int) returns (index : int)
    ensures index >= 0 ==> index < a.Length ==> a[index] == key
    ensures index < 0 ==> forall j::0 <= j < a.Length ==> a[j] != key
    {
        var index := 0;
        while index < a.Length
        invariant 0 <= index < a.Length
        invariant forall j :: 0 <= j < index ==> a[j] != key
        {
            if a[index] == key {return;}
            index := index + 1;
        }
        index := -1;
    }
  • 寻找最大值的验证

    method FindMax(a:array<int>) returns(max:int)
    ensures forall j:: 0 <= j < a.Length ==> max >= a[j]
    {
        var i := 0;
    
        while i < a.Length
    
        invariant 0 <= i <= a.Length
        invariant forall j:int :: 0 <= j < i ==> max >= a[j]
    
        {
            if a[i] > max 
            {max := a[i];}
            i := i + 1;
        }
    }
    • 二分搜索的验证

      predicate sorted(a:array<int>)
      reads a;
      {
          forall j,k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
      }
      method BinarySearch(a:array<int>,key : int) returns (pos:int)
      requires a.Length > 0 && sorted(a)
      ensures pos >= 0 ==> pos < a.Length && a[pos] == key;
      ensures pos < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
      {
          var l , r := 0 , a.Length;
          while l < r
          decreases r - l
          invariant 0 <= l <= r <= a.Length
          invariant forall i :: 0 <= i < a.Length && (i < l || i >= r) ==> a[i] != key
          {
              var mid := (l + r) / 2;
              if a[mid] == key
              {
                  return mid;
              }
              else if a[mid] > key
              {
                  r := mid;
              }
              else 
              {
                   l := mid + 1;
              }
          }
          return -1;
      }
      
  • 快速排序

    
    method Main() 
    {
         // intro local var - 6.1
         var a := new int[3]; // 3 element array of ints
         a[0], a[1], a[2] := 8, 6, 4;
         QuickSort(a,0,3);
         print "the sorted version of [4,8,6] is ";
         print a<int>;
         assert sorted(a,0,2);
         print "\ndone.";
         
         var q := new int[5]; // 3 element array of ints
         q[0], q[1], q[2] , q[3] , q[4] := 3, 2, 7 , 6 , 1;
         QuickSort(q,0,5);
         print "the sorted version of [1,2,3,6,7] is ";
         print a;
         assert sorted(q,0,4);
         print "\ndone.";
    }
    
    predicate sorted (a: array<int> ,low: int , high :int )
       requires a != null;
       requires 0 <= low <= high <= a.Length;
       reads a;
    {
        forall j,k ::low <= j < k < high ==> a[j] <= a[k]
    }
    
    
    method QuickSort(a: array<int>, start: int, end: int)
       requires a != null && a.Length >= 1;
       requires 0 <= start <= end <= a.Length; 
       requires 0 <= start <= end < a.Length ==> forall j :: start <= j < end ==> a[j] < a[end];
       requires 0 < start <= end <= a.Length ==> forall j :: start <= j < end ==> a[start - 1] <= a[j];
       modifies a;
       ensures sorted(a, start, end);
       ensures forall j :: 0 <= j < start || end <= j < a.Length ==> old(a[j]) == a[j];
       ensures 0 <= start <= end < a.Length ==> forall j :: start <= j < end ==> a[j] < a[end];
       ensures 0 < start <= end <= a.Length ==> forall j :: start <= j < end ==> a[start - 1] <= a[j];
       decreases end - start;
    {
        // alternation - 4.1
         if(end - start > 1)
         {
             var pivot := partition(a, start, end);
             QuickSort(a, start, pivot);
             QuickSort(a, pivot + 1, end);
         }
         else
         {
             return;
         }
    }
    
    method partition(a: array<int>, start: int, end: int) returns (pivot: int)
        requires a != null && a.Length > 0;
        requires 0 <= start < end <= a.Length;
        requires 0 <= start <= end < a.Length ==> forall j :: start <= j < end ==> a[j] < a[end];
        requires 0 < start <= end <= a.Length ==> forall j :: start <= j < end ==> a[start - 1] <= a[j];
        modifies a;
        ensures 0 <= start <= pivot < end <= a.Length;
        ensures forall j :: start <= j < pivot ==> a[j] < a[pivot];
        ensures forall j :: pivot < j < end ==> a[pivot] <= a[j];
        ensures forall j :: 0 <= j < start || end <= j < a.Length ==> old(a[j]) == a[j];
        ensures 0 <= start <= end < a.Length ==> forall j :: start <= j < end ==> a[j] < a[end];
        ensures 0 < start <= end <= a.Length ==> forall j :: start <= j < end ==> a[start - 1] <= a[j];
    {
         pivot := start;
         // intro local var - 6.1 + assignment - 1.3
         var index := start + 1; 
         // iteration - 5.5
         while(index < end)
                invariant start <= pivot < index <= end;
             invariant forall j :: start <= j < pivot ==> a[j] < a[pivot];
             invariant forall j :: pivot < j < index ==> a[pivot] <= a[j];
             invariant forall j :: 0 <= j < start || end <= j < a.Length ==> old(a[j]) == a[j];
             invariant 0 <= start <= end < a.Length ==> forall j :: start <= j < end ==> a[j] < a[end];
             invariant 0 < start <= end <= a.Length ==> forall j :: start <= j < end ==> a[start - 1] <= a[j];
         {
             // alternation - 4.1
             if(a[index] < a[pivot]) 
             {
                 assert 0 < start <= end <= a.Length ==> forall j :: start <= j < end ==> a[start - 1] <= a[j];
                 var counter := index - 1;
                 var temp := a[index];
                 a[index] := a[counter];
                 // iteration - 5.5
                 while(counter > pivot)
                     invariant forall j :: start <= j < pivot ==> a[j] < a[pivot];
                     invariant forall j :: pivot < j < index + 1 ==> a[pivot] <= a[j];
                     invariant a[pivot] > temp;
                     invariant forall j :: 0 <= j < start || end <= j < a.Length ==> old(a[j]) == a[j];
                     invariant 0 <= start <= end < a.Length ==> forall j :: start <= j < end ==> a[j] < a[end];
                     invariant 0 < start <= end <= a.Length ==> forall j :: start <= j < end ==> a[start - 1] <= a[j];
                 {
                     a[counter + 1] := a[counter];
                     counter := counter - 1;
                 }
                 a[pivot + 1] := a[pivot];
                 pivot := pivot + 1;
                 a[pivot - 1] := temp;
             }
             index := index + 1;
         }
    }
文章名: 《Dafny笔记》
文章链接:http://hrhr7.cn/index.php/archives/11/
联系方式:tensor7@163.com
除特别注明外,文章均为Cupidr原创,转载时请注明本文出处及文章链接
Last modification:July 21st, 2019 at 03:50 pm
如果觉得我的文章对你有用,请随意赞赏

Leave a Comment