For vs While

[KihongHeo]

I am trying to prove a simple property of linear search. Below are the two implementations using for and loop.

However, the while version is verified but the for version is not proved.
Is there any difference between these two?

method LinearSearch(a: array<int>, l: int, u: int, e: int) returns (b: bool)
  requires 0 <= l <= u < a.Length
  ensures b == (exists i: int :: l <= i <= u && a[i] == e)
{
  for i := l to u
    invariant l <= i <= u + 1
    invariant (forall j :: l <= j < i ==> a[j] != e)
  {
    if (a[i] == e) {
      return true;
    }
  }
  return false;
}

method LinearSearch(a: array<int>, l: int, u: int, e: int) returns (b: bool)
  requires 0 <= l <= u < a.Length
  ensures b == (exists i: int :: l <= i <= u && a[i] == e)
{
  var i := l;
  while i <= u
    invariant l <= i <= u + 1
    invariant (forall j :: l <= j < i ==> a[j] != e)
  {
    if (a[i] == e) {
      return true;
    }
    i := i + 1;
  }
  return false;
}

[keyboardDrummer]

for i := l to u excludes the end, so u is excluded. In your while loop though, u is included. If you change for i := l to u to for i := l to u + 1, it'll verify. You can find the precise meaning of the for statement in the documentation: https://dafny.org/dafny/DafnyRef/DafnyRef#g-for-statement

[KihongHeo]

Thanks.