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

original.name="RecursiveType_Valid_28"
======
>>> main.whiley
type Link is {
    int data,
    LinkedList next
}

type LinkedList is null | Link

// index i is "within bounds" of ls
property within(Link ls, int i) -> (bool r):
    // posiive index must be recurisvely satisfied    
    return (i > 0 && ls.next is Link && within(ls.next,i-1)) ||
           // index within bounds
           i == 0

function get(Link ls, int i) -> int
// Index i is within bounds
requires within(ls,i):
    //
    if i == 0:
        return ls.data
    else:
        // Following assertion required retyping ls
        assert ls.next is Link
        //
        return get(ls.next,i-1)

public export method test():
    LinkedList l1 = null
    Link l2 = { data: 1, next: l1 }
    Link l3 = { data: 2, next: l2 }
    //
    assume get(l2,0) == 1
    assume get(l3,0) == 2
    assume get(l3,1) == 1

---