{m:int | m >= 1}
unit initnext(plen: int(m), pat[m]: int, next[m]: [n:int | n >= -1] int(n)) {
  var: int i, j;;

  i = 0; j = -1;
  
  while (true) {
    if ( j == -1 || pat[i] == pat[j]) {
      i = i + 1; j = j + 1;
      if (i < plen) next[i] = j; else break;
    } else j = next[j];
  }
}

{m:int | m >= 1}
int kmpsearch(pat[m]: int, text[]: int) {
  var: int plen, tlen; int i, j;
       next[]: [n:int | n >= -1] int(n);;

  plen = arraysize(pat);
  tlen = arraysize(text);
  next = newarray(plen, 0);

  i = 0; j = 0; initnext (plen, pat, next);

  invariant: [i:nat, j:int | j >= -1] (i: int(i), j: int(j))
  while (i < plen && j < tlen) {
    if (j < 0 || text[i] == pat[j]) {
      i = i + 1; j = j + 1;
    } else j = next[j];
  }

  if (i > tlen) return -1; else return (i - plen);
}