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="While_Valid_26"
======
>>> main.whiley


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

function search(int[] items, int item) -> (null|nat result)
// The input list must be in sorted order
requires all { i in 0 .. |items|-1 | items[i] < items[i+1] }
// If the answer is an integer, then it must be a value index
ensures (result is nat) ==> items[result] == item
// If the answer is null, then the item must not be contained
ensures (result == null) ==> all { i in 0..|items| | items[i] != item }:
    //
    nat i = 0
    while i < |items|
        where i <= |items|
        where all { j in 0 .. i | items[j] != item }:
        //
        if items[i] == item:
            return i
        i = i + 1
    //
    return null

public export method test():
    int[] list = [3,5,6,9]
    assume search(list,0) == null
    assume search(list,1) == null
    assume search(list,2) == null
    assume search(list,3) == 0
    assume search(list,4) == null
    assume search(list,5) == 1
    assume search(list,6) == 2
    assume search(list,7) == null
    assume search(list,8) == null
    assume search(list,9) == 3
    assume search(list,10) == null

---