Dafny: не найдено условий, вызывающих срабатывание сообщения об ошибке

У меня есть массив 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;.

Моя логика для цикла заключается в том, что пока они находятся в цикле, индекс не был найден. И гарантирует, что когда он столкнулся с index.

Что может быть не так?

Вот код:

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.


formal-verification dafny
person pmpc    schedule 04.04.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Я не думаю, что вам нужно использовать квантификаторы, чтобы делать эти проблемные утверждения:

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

person lexicalscope    schedule 05.04.2016