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

original.name="While_Valid_21"
======
>>> main.whiley


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

function create(nat count, int value) -> (int[] result)
// Returned list must have count elements
ensures |result| == count:
    //
    int[] r = [0; count]
    int i = 0
    while i < count where i <= count && i >= 0 && count == |r|:
        r[i] = value
        i = i + 1
    return r

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

---