时间戳

首页 > 解决方案 > Dafny，如果在循环的进入和退出时断言为真，它是否是不变量

dafny - Dafny，如果在循环的进入和退出时断言为真，它是否是不变量

问题描述

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

最近被引导到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>, me: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,el,i);}
         (r ==> containsMe(l[..i+1],el)) ;
        }
        assert  (r ==>  containsMe(l[..i+1],el) ); /* true on exit */
    }
}

标签： dafnyloop-invariant

解决方案

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

invariant r ==> i < |l|

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

推荐阅读