2

line長さ の文字列が含まれる配列があります。これはl、 pat長さ の文字列が含まれる別の配列です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;
}

次のエラーが表示されます: Dafny 出力のスクリーンショット

これが rise4funのコードです。

4

1 に答える 1