Finding Triggers

[DavePearce]

property sorted_a(int[] xs)
where |xs| == 0 || all { i in 1 .. |xs| | xs[i-1] < xs[i] }

property sorted_b(int[] xs)
where all { i in 0 .. |xs|, j in 0..|xs| | (i < j) ==> xs[i] < xs[j] }

method f(int[] xs) -> (int[] ys)
requires sorted_a(xs)
ensures sorted_b(ys):
    return xs

Presumably it needs a lemma. This is an interesting one because it shows up differences in the difficulty of quantified formulae. I guess the other question is: does a trigger help?

[DavePearce]

See also boogie-org/boogie#441

[DavePearce]

This doesn't verify:

// In-place reverse of items in an array
function reverse(int[] xs) -> (int[] ys)
// Returned array is same size as input
ensures |xs| == |ys|
// All items in return array in opposite order
ensures all { i in 0..|xs| | xs[i] == ys[|xs|-(i+1)]}:
    //
    int n = |xs| - 1
    int i = 0
    int j = n
    int[] zs = xs
    //
    while i < j
    where i >= 0 && j == (n - i) && |zs| == |xs|
    where all { k in 0..i | xs[k] == zs[n-k] }:
        //
        int tmp = xs[i]
        xs[i] = xs[j]
        xs[j] = tmp
        j = j - 1
        i = i + 1
    //
    return xs 

[DavePearce]

Here is the boogie for the first example above:

procedure test(xs:[int]int)
{
   assume (forall i:int :: xs[i-1] < xs[i]);
   //
   assert (forall i:int, j:int :: (i < j) ==> (xs[i] < xs[j]));
}

Observe that the other way around works. See also boogie-org/boogie#451