A common array element method verified by Microsoft's Dafny from http://rjoshi.org/cs116/homework/hw1-common.dfy

dafny-find-common

/*
 * We are given 3 arrays a,b,c of integers sorted in ascending order, and we are told 
 * that there is a value that occurs in all three arrays. Write a Dafny program to 
 * compute the index in each array where the common value occurs.
 *
 * This is the best implementation I can come up with for this problem, however it
 * is still not verifiable by Dafny. It is a combination of the loop invariants or
 * ensures that seem to fail based on various permutations of saying that p,q,r are
 * < or <= a.Length,b.Length,c.Length, respectively. The long requires statement and
 * the identical assume statement have been added to keep the previously mentioned
 * statements from being violated, however they seem to have no effect. It would seem
 * that the addition of either or both of these statements would take care of the
 * violations, but these seem to simply be ignored. The problem is that the problem
 * description assumes that no matter what the arrays are, there will be some match
 * across them. I feel that I have captured this specification in the requires and
 * assume statement, but Dafny feels otherwise.
 */
method findCommon(a:array<int>, b:array<int>, c:array<int>) returns (p:int, q:int, r:int)
  requires a != null && 0 < a.Length;
  requires b != null && 0 < b.Length;
  requires c != null && 0 < c.Length;
  requires exists i,j,k :: 0 <= i < a.Length && 0 <= j < b.Length && 0 <= k < c.Length && a[i] == b[j] && b[j] == c[k];
  ensures 0 <= p < a.Length;
  ensures 0 <= q < b.Length;
  ensures 0 <= r < c.Length;
  ensures a[p] == b[q] && b[q] == c[r]; 
{
  assume exists i,j,k :: 0 <= i < a.Length && 0 <= j < b.Length && 0 <= k < c.Length && a[i] == b[j] && b[j] == c[k];
  p := 0;
  while(p < a.Length)
    invariant 0 <= p < a.Length;
    decreases a.Length - p;
  {
    q := 0;
    while(q < b.Length)
      invariant 0 <= q <= b.Length;
      decreases b.Length - q;
    {
      if(a[p] == b[q]) {
        r := 0;
        while(r < c.Length)
          invariant 0 <= r <= c.Length;
          decreases c.Length - r;
        {
          if(a[p] == c[r]) {
            return;
          }
          r := r+1;
        }
      }
      q := q+1;
    }
    p := p+1;
  }
}