Lemmas in Whiley?

Question

Based on an example I've done in Dafny, I was wondering how to prove similar things in Whiley? I worked out the new syntax for properties and came up with this:

property sum(int[] items, int i) -> (int r):
   if i < 0 || i >= |items|:
      return 0
   else:
      return items[i] + sum(items,i+1)

Now, my question is: how can I write a lemma in Whiley, like you can in Dafny? For example, to show that after an account transfer the total sum of all accounts is unchanged? I can't seem to find syntax for this.

Answer 1

Whiley does not currently have syntax for expressing lemmas like Dafny. However, as a work around, we can achieve the same effect with a function. Suppose I want to exploit a simple property of sums, like this:

// Set ith index to zero
function zeroOut(int[] xs, int i) -> (int[] ys)
requires 0 <= i && i < |xs|
// Sum decreased by appropriate amount
ensures sum(xs,0) - xs[i] == sum(ys,0):
    //
    xs[i] = 0
    //
    return xs

This does not verify as is. To get this to verify requires some intervention from us (i.e. introducing a lemma). We need to show sum(xs,0) == xs[i] + sum(xs[i:=0],0) where 0 <= i && i < |xs|. To do this ended up requiring two lemmas:

function lemma1(int[] xs, int[] ys, int k)
requires |xs| == |ys|
requires 0 <= k && k <= |xs|
requires all { i in k .. |xs| | xs[i] == ys[i] }
ensures sum(xs,k) == sum(ys,k):
    if k == |xs|:
        // base case
    else:
        lemma1(xs,ys,k+1)

function lemma2(int[] xs, int i, int k)
requires 0 <= k && k <= i && i < |xs|
ensures sum(xs,k) == xs[i] + sum(xs[i:=0],k):
    if i == k:
        // base case
        lemma1(xs,xs[k:=0],k+1)
    else:
        lemma2(xs,i,k+1)

You can see the conclusion of lemma2 is what we are trying to show. Notice that neither of the lemmas has a return value! This is perhaps a slight abuse of the syntax for Whiley, but it is convenient for now until explicit lemma syntax is added.

Finally, we can verify our original program by exploiting the lemma as follows:

function zeroOut(int[] xs, int i) -> (int[] ys)
requires 0 <= i && i < |xs|
// Sum decreased by appropriate amount
ensures sum(xs,0) - xs[i] == sum(ys,0):
    //
    lemma2(xs,i,0)
    xs[i] = 0
    //
    return xs

That works! However, it wasn't easy for me to figure out these lemmas would do it. Generally, it is something of a trial-and-error process (and this would hold for tools like Dafny as well) since we don't know what the automated theorem prover can handle at any given step.