Dafny如果在循环的入口和出口断言为真，则它是不变的

问题描述

在Dafny中，我正在尝试编写针对递归规范的迭代实现。更具体地说，当predicate containsMe<T (==)>(l:seq<T>,me:T) 是序列me的元素时，l返回true。

最近针对http://leino.science/papers/krml275.html，我发现其他方法可能会更好，尽管我偶然发现了一个有趣的问题。

我有一个部分解决方案（如下所述），可以验证在循环开始和结束处给出的断言，但这不是不变的。我是否错过了某些东西，这是一个错误还是有一种方法可以帮助Dafny建立我不了解的不变量？

predicate method containsMe<T (==)>(l:seq<T>,me:T) 
decreases l
{
  if l== [] then  false
    else if l[0] == me  then true else containsMe(l[1..],me)
}

lemma {:induction l} cont<T (==)>(l:seq<T>,me:T) 
   ensures (exists i:nat :: i<|l| && l[i] == me)  <==> containsMe(l,me)  { }

lemma {:induction l} conti<T (==)>(l:seq<T>,me:T,i:nat) 
   ensures ( i<|l| && l[i] == me)  ==> containsMe(l,me)  {
    calc {
      i<|l| && l[i] == me ;
      ==>
      exists i:nat :: i<|l| && l[i] == me;
      ==> {cont(l,me);}
      containsMe(l,me);
    }
    }
    
lemma  ping<T (==)>(l:seq<T>,i:nat) 
  ensures ( i<|l| && l[i] == me) ==> containsMe(l[..i+1],me)  
  { 
       calc {
         i<|l| && l[i] == me;
         ==>
         (i< |l[..i+1]| && l[..i+1][i] == me);
         ==> {conti(l[..i+1],me,i);}
          containsMe(l[..i+1],me);
       }        
  } 
 
method contains<T (==)>(l:seq<T>,el:T) returns (r:bool)
//ensures r == containsMe(l,el)
{
    print "contains ",l,",el,"\n";
    var i:nat:= 0;
    r := false;
    while (i < |l| && r ==false)
       decreases  |l| -i,!r
       invariant (r ==> containsMe(l[..i+1],el) ) /*fails to verify */
    {
       assert    (r ==> containsMe(l[..i+1],el) );  /* true on entry */
        var b:bool := containsMe(l[..i+1],el);
        print "  ",i,"  ",l[i]," ",b,"\n";        
        if l[i] == el {
            r:=true; }
        else {i := i+1;}       
        calc { 
          (r==>  i<|l| && l[i] == el);
             ==> {ping(l,i);}
         (r ==> containsMe(l[..i+1],el)) ;
        }
        assert  (r ==>  containsMe(l[..i+1],el) ); /* true on exit */
    }
} 

解决方法

Dafny并未抱怨不变量不变。它抱怨它的格式不正确，因为它认为索引i+1可能大于数组的长度。添加

invariant r ==> i < |l|

在其他不变式解决该问题之前。