=====
>>> main.whiley
property sum(int[] items, int i) -> (int r):
if i < 0 || i >= |items|:
return 0
else:
return items[i] + sum(items,i+1)
function create() -> (int[] xs, int s)
ensures |xs| > 0
ensures s == sum(xs,0):
return ([1,2,3],6)
public export method test():
(int[] vs, int s) = create()
// Copy array (as ghost)
int[] ws = vs
// Increase overall sum
vs[0] = vs[0] + 1
//
assert sum(vs,0) > s
---
E722 main.whiley 19,11:23
=====
>>> main.whiley 12:20
function lemma_1(int[] xs, int[] ys, int i)
// Arrays must have same size
requires |xs| == |ys|
// Index must be within bounds
requires i >= 0 && i <= |xs|
// Everything beyond this is the same
requires all { k in i..|xs| | xs[k] == ys[k] }
// Conclusion
ensures sum(xs,i) == sum(ys,i):
//
if i == |xs|:
// base case
else:
lemma_1(xs,ys,i+1)
// Index i identifies position within the two arrays which differ.
// Index j is current index through arrays (starting from zero).
function lemma_2(int[] xs, int[] ys, int i, int j)
// Arrays must have same size
requires |xs| == |ys|
// Indices must be within bounds
requires j >= 0 && j <= i && i < |xs|
// Everything else must be same
requires all { k in 0..|xs| | k == i || xs[k] == ys[k] }
// Ith element must have increased
requires xs[i] < ys[i]
// Conclusion
ensures sum(xs,j) < sum(ys,j):
//
if j < i:
lemma_2(xs,ys,i,j+1)
else:
lemma_1(xs,ys,i+1)
public export method test():
(int[] vs, int s) = create()
// Copy array (as ghost)
int[] ws = vs
// Increase overall sum
vs[0] = vs[0] + 1
// Check this
lemma_2(ws,vs,0,0)
//
assert sum(vs,0) > s
---