时间戳

首页 > 解决方案 > 为什么这个 Dafny 示例验证失败？

dafny - 为什么这个 Dafny 示例验证失败？

问题描述

这是一个学习 Dafny 的例子。

method test5(x:array<int>,y:array<int>,n:int)
requires 0<=n
requires 0< x.Length
requires 0< y.Length  
requires x[0]==y[0]; 
requires (x[0]>=0 ==> y[0]>=0)
requires  (y[0]>= 0 ==> x[0]>= 0)
requires  (x[0]+y[0]==0 || x[0]+y[0]>0);
modifies y;  
modifies x; 
ensures  (x[0]==y[0]); 
ensures (x[0]>0 ==> y[0]>0)
ensures (y[0] > 0 ==> x[0] > 0)
ensures  (x[0]+y[0]==0 || x[0]+y[0]>0)     
{     if (x[0]>0)
    {x[0]:=x[0]- 1; 
     y[0]:=y[0]- 1;
     }
}

为什么验证失败？

达夫尼可以举一个反例吗？

标签： dafny

解决方案

是的，你可以举个反例。如果您使用的是 Visual Studio，只需单击错误所在的红色圆圈。这将打开验证调试器。如果您使用的是 VS Code，请按 F7（请参阅https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode）。这将重新验证您的程序并向您展示反例中的一些信息。

在您的情况下，这些反例显示x和最初y是相等的。x[0]==y[0]==1实际上，从那个初始状态开始，test5不会建立其声明的后置条件。

鲁斯坦

推荐阅读