whiley_test_file 0.6.2

An API for manipulating test files for the Whiley Programming Language.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

original.name="Property_Valid_9"
======
>>> main.whiley
property sum(int n, int[] xs, int i) -> (bool r):
    return (i >= |xs| && n == 0) ||
           (i >= 0 && i < |xs| && sum(n-xs[i],xs,i+1))

function fsum(int[] xs, int s, int[] ys) -> (int r)
requires sum(s,xs,0) && sum(s,ys,0)
ensures r == 0:
    //
    return 0

function f() -> (int r):
    return 123678

public export method test():
    int x = f()
    //
    assert fsum([1],1,[1]) == 0
    assert fsum([1],1,[1,0]) == 0
    assert fsum([1,0],1,[1]) == 0
    assert fsum([1,2],3,[1,2]) == 0
    assert fsum([2,1],3,[1,2]) == 0
    assert fsum([1,2],3,[2,1]) == 0
    assert fsum([1,2],3,[1,1,1]) == 0
    assert fsum([1,1,1],3,[1,2]) == 0
    assert fsum([1,1,1],3,[1,1,1]) == 0
    assert fsum([x,x],2*x,[x,x]) == 0
---