Dafny錯誤消息

Question

我有一個具有包含在其長度l的字符串， pat陣列line「沒有發現觸發條件」是具有包含在其長度p的字符串另一個陣列。 注：p和l不是陣列

目的是看看是否包含在pat字符串中存在line的長度。如果是這樣，這個方法應該返回該單詞的第一個字母的line索引，如果不是，它應該返回-1。

所給予我們的「發現觸發沒有條件」的不變量誤差ensures exists j :: (0<= j < l) && j == pos;和invariant forall j :: 0 <= j < iline ==> j != pos;

我對循環邏輯是，雖然他們是在循環索引沒有被發現。確保是在遇到索引時。

什麼可能是錯的？

下面是代碼：

method find(line:array<char>, l:int, pat:array<char>, p:int) returns (pos:int) 
requires line!=null && pat!=null; 
requires 0 <= l < line.Length; 
requires 0 <= p < pat.Length; 
ensures exists j :: (0<= j < l) && j == pos; 

{ 

var iline:int := 0; 
var ipat:int := 0; 
var initialPos:int := -1; 

while(iline<l && ipat<pat.Length) 
invariant 0<=iline<=l; 
invariant 0<=ipat<=pat.Length; 
invariant forall j :: 0 <= j < iline ==> j != pos; 

{ 
    if(line[iline]==pat[ipat] && (line[iline]!=' ' && pat[ipat]!=' ')){ 
     if(initialPos==-1){ 
      initialPos := iline; 
     } 
     ipat:= ipat + 1; 
    } 
    else{ 
    if(ipat>0){ 
     if(line[iline] == pat[ipat-1]){ 
     initialPos := initialPos + 1; 
     } 
    } 
     ipat:=0; 
     initialPos := -1; 
    } 
    if(ipat==p){ 
     return initialPos; 
    } 
    iline := iline + 1; 
} 
return initialPos; 
} 

我收到以下錯誤： screenshot of Dafny output

這裏是the code on rise4fun。

Answer 1

我不認爲你需要使用量詞，使那些有問題的主張：

exists j :: (0<= j < l) && j == pos; 

可以更好地寫爲：

0 <= pos < l 

而且

forall j :: 0 <= j < iline ==> j != pos 

有意思相同：

pos >= iline 

通過刪除您刪除的量詞，解算器需要實例化量詞，因此不需要觸發器。

此外，我認爲你的方法將返回-1如果沒有找到模式。所以，你需要考慮的是，使其驗證：

method find(line:array<char>, l:int, pat:array<char>, p:int) returns (pos:int) 
    requires line!=null && pat!=null 
    requires 0 <= l < line.Length 
    requires 0 <= p < pat.Length 
    ensures 0 <= pos < l || pos == -1 
{ 
    var iline:int := 0; 
    var ipat:int := 0; 
    pos := -1; 

    while(iline<l && ipat<pat.Length) 
    invariant 0<=iline<=l 
    invariant 0<=ipat<=pat.Length 
    invariant -1 <= pos < iline 
    { 
     if(line[iline]==pat[ipat] && (line[iline]!=' ' && pat[ipat]!=' ')){ 
      if(pos==-1){ 
       pos := iline; 
      } 
      ipat:= ipat + 1; 
     } else { 
     if(ipat>0){ 
      if(line[iline] == pat[ipat-1]){ 
      pos := pos + 1; 
      } 
     } 
     ipat:=0; 
     pos := -1; 
     } 
     if(ipat==p) { 
      return; 
     } 
     iline := iline + 1; 
    } 
    return; 
} 

http://rise4fun.com/Dafny/J4b0