经验首页 前端设计 程序设计 Java相关 移动开发 数据库/运维 软件/图像 大数据/云计算 其他经验
当前位置:技术经验 » 其他 » 业界动态 » 查看文章
dafny : 微软推出的形式化验证语言
来源:cnblogs  作者:tianxiaozz  时间:2022/11/19 17:14:02  对本文有异议

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

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

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

点击查看代码
  1. method Abs(x: int) returns(y: int)
  2. ensures y >= 0 && (|| y == x || y == -x)
  3. {
  4. return if x > 0 then x else -x;
  5. }

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

点击查看代码
  1. method Find(a: array<int>, v: int) returns(index: int)
  2. ensures 0 <= index ==> index < a.Length && a[index] == v
  3. ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != v
  4. {
  5. var i : int := 0;
  6. while i < a.Length
  7. invariant 0 <= i <= a.Length
  8. invariant forall k :: 0 <= k < i ==> a[k] != v
  9. {
  10. if a[i] == v {
  11. return i;
  12. }
  13. i := i + 1;
  14. }
  15. return -1;
  16. }

这个算法是要找数组里面的某个数,找到了就返回下标,否则返回-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

while循环第二个后置条件,保障了Find函数第二个后置条件。

vscode的编辑器能实时验证算法是否正确,这对于编写dafny代码十分有利。

原文链接:https://www.cnblogs.com/tianxiaozz/p/16905921.html

 友情链接:直通硅谷  点职佳  北美留学生论坛

本站QQ群:前端 618073944 | Java 606181507 | Python 626812652 | C/C++ 612253063 | 微信 634508462 | 苹果 692586424 | C#/.net 182808419 | PHP 305140648 | 运维 608723728

W3xue 的所有内容仅供测试,对任何法律问题及风险不承担任何责任。通过使用本站内容随之而来的风险与本站无关。
关于我们  |  意见建议  |  捐助我们  |  报错有奖  |  广告合作、友情链接(目前9元/月)请联系QQ:27243702 沸活量
皖ICP备17017327号-2 皖公网安备34020702000426号