Dafny "no terms found to trigger on" error message

Question

I have an array line that has a string contained in it of length l, pat is another array that has a string contained in it of length p. Note: p and l are not the length of the arrays

The objective is to see if the string contained in pat exists in line. If so, this method should return the index in line of the first letter of the word, if not it should return -1.

The invariants that are giving us the "no terms found to trigger on" errors are ensures exists j :: ( 0<= j < l) && j == pos; and invariant forall j :: 0 <= j < iline ==> j != pos;

My logic for the loop is that while they are in the loop the index wasn't found. And the ensures is when it encountered an index.

What could possible be wrong?

Here is the 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;
}

I'm receiving the following errors: screenshot of Dafny output

Here is the code on rise4fun.

Answer 1

I don't think you need to use quantifiers to make those problematic assertions:

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

Could be better written as:

0 <= pos < l

And

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

Has the same meaning as:

pos >= iline

By removing the quantifiers you removed the need for the solver to instantiate the quantifier, and therefore no trigger is needed.

Also, I think your method will return -1 if the pattern is not found. So you will need to account for that to make it verify:

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