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

original.name="For_Valid_7"
======
>>> main.whiley
// Define a predicate type
public type pred_t is function(int)->bool

// Sum elements matching predicate
public function filter(int[] items, pred_t fn) -> (int[] rs)
ensures |rs| <= |items|:
    int n = 0
    // Determine how many
    for i in 0..|items| where 0 <= n && n <= i:
        if fn(items[i]):
            n = n + 1
    // Allocate space
    int[] nitems = [0;n]
    int j = 0
    // Copy them over
    for i in 0..|items| where |nitems| <= |items| && j >= 0:
        int ith = items[i]
        if fn(ith):
            assume j < |nitems|
            nitems[j] = ith
            j = j + 1
    // Done
    return nitems

public export method test():
    assume filter([-1,0,1,2,3],&(int x -> x > 0)) == [1,2,3]
    assume filter([-3,-2,-1],&(int x -> x >= 0)) == []
    assume filter([0,1,2,3],&(int x -> x >= 0)) == [0,1,2,3]

---