Dafny无法自动证明特定断言，如何无需额外断言实现验证

问题背景 #

以下是编写的Dafny程序：

predicate Q (x:int,y:int)
{
x == y
}

function F (j:int,s:seq<int>):int
requires 0 <= j < |s|-1
{
s[j+1] 
}

predicate Pi (i: nat, s:seq<int>)
   requires 1 <= i < |s|
{
Q(s[i-1],F(i-1,s))
}


predicate P (s:seq<int>)
{
forall i :: 1 <= i < |s| ==> Pi(i,s)
}

method checkforall (s:seq<int>) returns (b:bool)
requires |s| > 1
ensures b <==> P(s)
{
var j := 1;
b := true;
while j < |s| && Pi(j,s)
   invariant 0 <= j <= |s|
   invariant b <==> forall  i :: 1 <= i < j ==> Pi(i,s)  
   {
      j := j+1;
   }
if j < |s| 
   {
      b := false;
   }
}

method Main()
{
var s := [0,0,0,0,0];
var b := checkforall(s);
assert b;  
}

该程序的Main方法可正常验证，但以下Main方法无法通过验证：

method Main()
{
var s := [0,1,0,0,0];
var b := checkforall(s);
assert !b;  
}

当前需要手动添加assert !Pi(2,s)才能完成证明，现需解决无需添加该额外断言即可通过验证的问题。

解决方案 #

方案1：利用循环终止逻辑添加通用断言 #

在checkforall方法中，当循环退出后、设置b := false之前，添加一个基于循环终止条件的通用断言：

method checkforall (s:seq<int>) returns (b:bool)
requires |s| > 1
ensures b <==> P(s)
{
var j := 1;
b := true;
while j < |s| && Pi(j,s)
   invariant 0 <= j <= |s|
   invariant b <==> forall  i :: 1 <= i < j ==> Pi(i,s)  
   {
      j := j+1;
   }
if j < |s| 
   {
      assert !Pi(j,s); // 循环终止的必然结果：若j < |s|，则Pi(j,s)不成立
      b := false;
   }
}

这个断言并非指定具体位置的硬编码断言，而是基于循环条件的逻辑推导——循环的继续条件是j < |s| && Pi(j,s)，因此当循环退出且j < |s|时，Pi(j,s)必然为假。添加该断言后，Dafny验证器可以利用这一事实，推导出b会被设为false，从而证明assert !b成立。

方案2：简化谓词定义，降低验证器推导难度 #

观察Pi的定义可以发现，它可以直接展开为更简洁的形式：

• F(i-1,s)的返回值是s[(i-1)+1] = s[i]
• Q(x,y)的含义是x == y

因此可以将Pi的定义直接简化，避免嵌套调用：

predicate Pi (i: nat, s:seq<int>)
   requires 1 <= i < |s|
{
s[i-1] == s[i] // 直接展开原有的Q和F调用
}

简化后，Dafny验证器无需额外展开多层函数/谓词的定义，就能直接识别Pi的含义，从而自动推导出当s = [0,1,0,0,0]时，Pi(2,s)为假，进而证明assert !b成立。

内容的提问来源于stack exchange，提问作者Montserrat Hermo