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
31
32
33
34
35
36
37
38
39
40
41

original.name="Complex_Valid_6"
======
>>> main.whiley


type nat is (int x) where x >= 0

function max(int a, int b) -> (int r)
ensures (r == a) || (r == b)
ensures (a <= r) && (b <= r):
    //
    if a < b:
        return b
    else:
        return a

function diff(int a, int b) -> (nat r)
ensures (r == a - b) || (r == b - a)
ensures ((a - b) <= r) && ((b - a) <= r):
    nat diff
    //
    if a > b:
        diff = a - b
    else:
        diff = b - a
    //
    return diff

public export method test() :
    int i = 0
    while i < 20:
        int j = 0
        while j < 20:
            assume i < j || diff(i-10,j-10) == (i - j)
            assume i > j || diff(i-10,j-10) == (j - i)
            j = j + 1
        //
        i = i + 1
    //

---