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

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

property sorted(int[] arr, int n) -> (bool r):
    return n >= 1 && n <= |arr| &&
           all { i in 1..n | arr[i-1] < arr[i] }

function create(int start, int end) -> (int[] result)
requires start < end
ensures sorted(result,|result|) && |result| == (end - start):
    //
    nat i = 1
    nat length = (end - start)
    int[] items = [start;length]
    //
    while i < length
    where i > 0 && |items| == length
    where sorted(items,i) && items[i-1] < (start+i):
        items[i] = start + i
        i = i + 1
    // Done
    return items

public export method test():
    //
    assume create(0,1) == [0]
    //
    assume create(0,2) == [0,1]
    //
    assume create(0,3) == [0,1,2]
    //
    assume create(1,4) == [1,2,3]
    //
    assume create(2,4) == [2,3]
    //
    assume create(3,4) == [3]

---