Dafny - Specifying that the largest element less than a given element is returned

Question

Goal

I wrote a method GetPredecessor(x, s) which takes a real number x and a sorted sequence of reals s. The input x is not necessarily a member of the sequence, but it is greater than or equal to the smallest member of the sequence, and less than or equal to the largest member of the sequence.

The output is supposed to be the largest member of the sequence that is less than the input (if possible).

Example

Let s = [1.0 2.0 3.0 4.0].

• For 3.0 < x <= 4.0 (e.g. x = 3.2, x = 3.8, x = 4.0), the output shall be 3.0 (not 1.0 or 2.0).
• For x = 1.0 there is no element in the sequence less than x, so the output shall be 1.0.

Question

I have been able to specify all preconditions and the following postconditions:

• if the input is equal to the smallest element of the sequence, return that
• if the input is larger than the smallest element of the sequence, the output will be less than the input

which is why the following assertions hold

var s := [1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0];
var r := 0.0;

r := GetPredecessor(1.0, s);
assert r == 1.0; // OK

r := GetPredecessor(3.2, s);
assert r <= 3.0; // OK

I have been unable to write the following postcondition:

• the output will be the largest element smaller than the input

which is why this assertion does not hold:

r := GetPredecessor(3.2, s);
assert r == 3.0; // FAILS

What do I need to do to specify the behaviour explained above, and how do I need to change the method body for the postcondition to hold on all return paths in the method?

Any help is greatly appreciated.

Code

Predicates and functions used in specifications

predicate Sorted(s: seq<real>)
{
    forall i,j :: 0 <= i < j < |s| ==> s[i] < s[j]
}

predicate Distinct(s: seq<real>)
{
    forall i,j :: 0 <= i < |s| && 0 <= j < |s| && i != j ==> s[i] != s[j]
}

function method Min(s: seq<real>) : (m: real)
    requires |s| > 0 && Sorted(s)
    ensures m in s
    ensures forall i :: 0 <= i < |s| ==> m <= s[i]
    ensures exists i :: 0 <= i < |s| && m == s[i]
{
    s[0]
}

function method Max(s: seq<real>) : (m: real)
    requires |s| > 0 && Sorted(s)
    ensures m in s
    ensures forall i :: 0 <= i < |s| ==> m >= s[i]
    ensures exists i :: 0 <= i < |s| && m == s[i]
{
    s[|s| - 1]
}

Main method / functionality

// returns the largest element in the sequence s that is smaller than input x; or Min(s), if x is Min(s)
method GetPredecessor(x: real, s: seq<real>) returns (r: real)
    requires |s| > 0 && Sorted(s) && Distinct(s)
    requires Min(s) <= x <= Max(s)
    ensures r in s
    ensures x == Min(s) ==> r == Min(s)
    ensures x != Min(s) ==> r < x
    // TODO: add postcondition -> not just any "predecessor" is returned, rather the largest of them
    {
        if x == Min(s)
        {
            return x;
        }

        var i := 0;
        r := s[i];

        while i < |s|
            invariant 0 <= i <= |s|
            invariant r in s
            invariant r < x
            decreases |s| - i
        {
            if r < s[i] < x
            {
                r := s[i];
            }

            i := i + 1;
        }    
    }

Answer 1

I think you need this predicate:

predicate LargestSmaller(x: real, s: seq<real>, returned: real)
{ 
  && returned in s
  && forall i | 0 <= i < |s| ::
        s[i] > returned ==> s[i] > x
}

Here is how you'd use it in your method definition:

method GetPredecessor(x: real, s: seq<real>) returns (r: real)
  ...
  ensures x != Min(s) ==> LargestSmaller(x, s, r)

Because you have a forall, you need to explicitly trigger it it if you want to prove your point:

      r := GetPredecessor(3.2, s);
      assert r == 1.0 || r == 2.0 || r == 3.0;
      var _, _ := s[1], s[2]; // Automatically instantiate the predicate to prove that r != 1.0 and r != 2.0, otherwise you'd get a contradiction.
      assert r == 3.0; // SUCCEEDS