Dafny „keine Begriffe auf auszulösen gefunden“ Fehlermeldung

Question

Ich habe line eine Anordnung, die eine Zeichenfolge in der es enthalten ist, weist Länge l, pat ist eine andere Anordnung, die eine Zeichenfolge enthalten ist darin der Länge p hat. Hinweis: p und l sind nicht die Länge der Arrays

Ziel zu sehen ist, wenn die Zeichenfolge in pat enthalten in line existiert. Wenn dies der Fall ist, sollte diese Methode den Index in line des ersten Buchstabens des Wortes zurückgeben, andernfalls sollte -1 zurückgegeben werden.

Die Invarianten, die uns die „keine Begriffe auf auslösen gefunden“ geben Fehler sind ensures exists j :: (0<= j < l) && j == pos; und invariant forall j :: 0 <= j < iline ==> j != pos;

Meine Logik für die Schleife, dass ist, während sie in der Schleife sind wurde der Index nicht gefunden. Und das ist sicher, wenn es einen Index gefunden hat.

Was könnte möglicherweise falsch sein? Hier

ist der Code:

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; 
} 

Ich erhalte die folgenden Fehler: screenshot of Dafny output

Hier ist the code on rise4fun.

Answer 1

ich Sie quantifiers verwenden müssen, um diese problematische Behauptungen glaube nicht, zu machen:

0 <= pos < l 

Und

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

Hat der:

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

könnte besser sein, als geschrieben gleiche Bedeutung wie:

pos >= iline 

Durch das Entfernen der Quantifizierer wurde die Instanziierung des Quantifizierers durch den Solver überflüssig. Daher ist kein Trigger erforderlich.

Auch ich denke, Ihre Methode wird -1 zurückgeben, wenn das Muster nicht gefunden wird.

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

: So müssen Sie für das Konto, um es überprüfen