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

original.name="Property_Valid_5"
======
>>> main.whiley
type nat is (int x) where x >= 0

property absent(int[] items, int item, nat end) -> (bool r):
    return end <= |items| && all { i in 0..end | items[i] != item }

function indexOf(int[] items, int item) -> (int r)
ensures (r >= 0) ==> (items[r] == item)
ensures (r < 0) ==> absent(items,item,|items|):
    //
    nat i = 0
    //
    while i < |items| where absent(items,item,i):
        if items[i] == item:
            return i
        i = i + 1
    //
    return -1

public export method test():
    int[] items = [4,3,1,5,4]
    assume indexOf(items,0) == -1
    assume indexOf(items,1) == 2
    assume indexOf(items,4) == 0
    
---