Dafny «не найдено условия для запуска на» сообщение об ошибке

Question

У меня есть массив, который имеет 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; 
} 

Я получаю следующие ошибки: 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