dafny : 微软推出的形式化验证语言 - tianxiaozz

1 year ago

source link: https://www.cnblogs.com/tianxiaozz/p/16905921.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.

dafny : 微软推出的形式化验证语言

dafny是一种可验证的编程语言，由微软推出，现已经开源。

dafny能够自我验证，可以在VS Code中进行开发，在编辑算法时，写好前置条件和后置条件，dafny验证器就能实时验证算法是否正确。

在官方的例子中，以Abs绝对值函数来进行说明，代码如下：

点击查看代码

method Abs(x: int) returns(y: int)

    ensures y >= 0 && (|| y == x || y == -x)

{

    return if x > 0 then x else -x;

}

Abs是方法名，x为形参，类型为int， y为返回值，类型为int。

Abs没有前置条件，只有一个后置条件ensures y >= 0 && (|| y == x || y == -x)，这样Abs返回值必须非负且y = x 或者 y = -x，定义了Abs的规约条件。

方法内就是具体的算法，根据x与0的比较，返回不同的值。

dafny语言里面有一个非常重要的后置条件写法，那就是loop。

下面举一个例子：

Verify the program in Algorithm 1. Note that you cannot change the existing implementation.

Algorithm 1 Find an element in array

点击查看代码

method Find(a: array<int>, v: int) returns(index: int)

    ensures 0 <= index ==> index < a.Length && a[index] == v

    ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != v

{

    var i : int := 0;

    while i < a.Length

        invariant 0 <= i <= a.Length

        invariant forall k :: 0 <= k < i ==> a[k] != v

    {

        if a[i] == v {

            return i;

        }

        i := i + 1;

    }

    return -1;

}

这个算法是要找数组里面的某个数，找到了就返回下标，否则返回-1。

这个算法有两个后置条件，分比对应找到了目标值和没有找到目标值，

找到了目标值，返回为非负值，返回值必须小于数组长度且数组对应值与目标值相等。

ensures 0 <= index ==> index < a.Length && a[index] == v

没有找到目标值，返回为负值，这就意味着数组里的所有值与目标值都不相等。

ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != v

这种写法用了形式化语言进行了规约。

算法实现很简单，while循环需要增加后置条件，

一个是i的范围，i的初值为0，循环退出时，i的值为数组长度。

invariant 0 <= i <= a.Length

while循环的另外一个后置条件，对于i，数组i前面的数字都与目标值不相等。

invariant forall k :: 0 <= k < i ==> a[k] != v