Implementation and Verification of two sum in Dafny

two_sum.dfy

predicate sorted (s: seq<int>)
{
  if |s| <= 1 then true else s[0] <= s[1] && sorted(s[1..])
}

lemma {:induction m, n} sorted_elem_lemma(s: seq<int>, m: int, n: int)
  decreases n - m
  requires sorted(s)
  requires 0 <= m <= n < |s|
  ensures s[m] <= s[n]
{
  if(m == n) {}
  else {
    sorted_elem_lemma(s, m+1, n);
    var i := 0;
    while i < m
      invariant i <= m < |s|
      invariant sorted(s[i..])
    {
      if( i == 0 ) {}
      else {
        assert sorted(s[(i+1)..]);
      }
      i := i + 1;
    }
  }
}

method find_indices (s: seq<int>, sm: int) returns (i: int, j: int)
  requires sorted(s)
  requires exists m, n :: 0 <= m < n < |s| && s[m] + s[n] == sm
  ensures 0 <= i < j < |s| && s[i] + s[j] == sm
{
  i := 0;
  j := |s| - 1;

  while i < j
    invariant 0 <= i <= j < |s|
    invariant exists m, n :: i <= m < n <= j && s[m] + s[n] == sm
    invariant forall m, n :: 0 <= m < i && m < n < |s| ==> s[m] + s[n] != sm
    invariant forall m, n :: j < n < |s| && 0 <= m < n ==> s[m] + s[n] != sm
  {
    if (s[i] + s[j] < sm){
      forall k | i < k < |s| ensures s[i] + s[k] != sm {
        if k <= j {
          sorted_elem_lemma(s, k, j);
          assert s[k] <= s[j];
          assert s[i] + s[k] <= s[i] + s[j];
        }
      }
      i := i + 1;
    }
    else if (s[i] + s[j] > sm){
      forall k | 0 <= k < j ensures s[k] + s[j] != sm {
        if i <= k {
          sorted_elem_lemma(s, i, k);
          assert s[i] <= s[k];
          assert s[i] + s[j] <= s[k] + s[j];
        }
      }
      j := j - 1;
    }
    else{
      return i, j;
    }
  }
}