Longest sequence that holds a property in Dafny

Question

In Dafny I am trying to make a Max polymorphic and high-order function that, given a sequence and a predicate, returns the longest subsequence that holds it. For instance, the longest increasing subsequence, or the longest subsequence in which all the elements are zero.

To do so, I designed a slow algorithm (given the P predicate and a S sequence):

   1. Start an i pivot in the left and a j pivot in the same place.
   2. Start the max_sequence = [] and the max_sequence_length = 0.
   3. While i<S.length:
        counter = 0 
        j = i
        While max_sequence[i..j] satisfies P and j<S.length:
          If counter > max_sequence_length:
             max_sequence_length = counter
             max_sequence = max_sequence[i..j]
          Increment j
        Increment i
   4. Return max_sequence

You can see it implemented:

method maxPropertySequence<T>(P: seq<T> -> bool, sequ: seq<T>) returns (max_seq: seq<T>)

  {
    var i := 0;
    var j := 0;
    var longest := 0;
    var the_sgmt := sequ;
    var fresh_segmnt := sequ;
    var counter := longest;
    while i<(|sequ|) 
      decreases |sequ|-i
    {
      j := i;
      counter := 0;
      fresh_segmnt := [sequ[i]];
      if P(fresh_segmnt) 
      {
          j := j+1;
          counter:=counter+1;
          if counter>longest {
            longest:=counter;
            the_sgmt := fresh_segmnt;
          }
          while P(fresh_segmnt) && j<|sequ|
            decreases |sequ|-j
          {
            fresh_segmnt := fresh_segmnt + [sequ[j]];
            j := j+1;
            counter:=counter+1;
            if counter>longest {
              longest:=counter;
              the_sgmt := fresh_segmnt;
            }
          }
      }
      i := i+1;
    }
    return the_sgmt;
      
  }

My question is: how can I verify that the Max function behaves as I expect? More concretely: which are the ensures I have to add?

I have thought something like: forall the subsequences of the original sequence, there is no subsequence that holds P and is longer than the_sgmt. But I do not know how to express it efficiently.

Thanks!

Answer 1

I wrote code for finding the (leftmost) longest subsequence of zeros from a given integer array. Since you can map sequ using the predicate, these two are almost identical problems.

// For a given integer array, let's find the longest subesquence of 0s.
// sz: size, pos: position.   a[pos..(pos+sz)] will be all zeros
method longestZero(a: array<int>) returns (sz:int, pos:int)   
    requires 1 <= a.Length
    ensures 0 <= sz <= a.Length
    ensures 0 <= pos < a.Length
    ensures pos + sz <= a.Length
    ensures forall i:int  :: pos <= i < pos + sz ==> a[i] == 0
    ensures forall i,j :: (0 <= i < j < a.Length && getSize(i, j) > sz) ==> exists k :: i <= k <= j && a[k] != 0
{
    var b := new int[a.Length];   // if b[i] == n, then a[i], a[i-1], ... a[i-n+1] will be all zeros and (i-n ==0 or a[i-n] !=0)
    if a[0] == 0
        {b[0] := 1;}
    else
        {b[0] := 0;}

    var idx:int := 0;
    while idx < a.Length - 1    // idx <- 0 to a.Length - 2
        invariant 0 <= idx <= a.Length - 1
        invariant forall i:int :: 0 <= i <= idx ==>  0 <= b[i] <= a.Length
        invariant forall i:int :: 0 <= i <= idx ==> -1 <= i - b[i]
        invariant forall i:int :: 0 <= i <= idx ==> (forall j:int :: i-b[i] < j <= i ==> a[j] == 0) 
        invariant forall i:int :: 0 <= i <= idx ==> ( 0 <= i - b[i] ==> a[i - b[i]] != 0 )
    {
        if a[idx + 1] == 0
            { b[idx + 1] := b[idx] + 1; }
        else
            { b[idx + 1] := 0;}

        idx := idx + 1;
    }


    idx := 1;
    sz := b[0];
    pos := 0;
    // Let's find maximum of array b. That is the desired sz.
    while idx < a.Length
        invariant 1 <= idx <= b.Length

        invariant 0 <= sz <= a.Length
        invariant 0 <= pos < a.Length
        invariant pos + sz <= a.Length

        invariant forall i:int :: 0 <= i < idx  ==> b[i] <= sz
        invariant forall i:int  :: pos <= i < pos + sz ==> a[i] == 0
        invariant forall i, j:int  :: (0 <= i < j < idx && getSize(i,j) > sz) ==>  a[j-b[j]] != 0
    {
        // find max
        if b[idx] > sz 
        { 
            sz := b[idx]; 
            pos := idx - b[idx] + 1;
        }
        idx := idx + 1;
    }
}


function getSize(i: int, j:int) : int
{
    j - i + 1    
}

Since I am new to dafny, any comments on style or anything are appreciated.