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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

original.name="Reference_Valid_24"
boogie.ignore=true
Whiley2Boogie.issue=89
======
>>> main.whiley
type uint is (int n) where n >= 0

// LIFO
type Channel<T> is {
    T[] slots,
    uint size
} where size <= |slots|

method put<T>(&Channel<T> self, T val, uint n):
    // Pseudo concurrency
    while n > 0 && self->size == |self->slots|:
        n = n - 1
    // Check what happened
    if n > 0:
        self->slots[self->size] = val
        self->size = self->size + 1

method get<T>(&Channel<T> self, T def, uint n) -> (T r):
    // Pseudo concurrency
    while n > 0 && self->size == 0:
        n = n - 1
    // Check what happened
    if n <= 0:
        // timeout
        return def
    else:
        self->size = self->size - 1    
        return self->slots[self->size]

final uint TIMEOUT = 100

public export method test():
    // Construct empty channel
    &Channel<int> ch = new { slots: [0,0,0], size: 0 }
    // Put some items in
    put(ch,1,TIMEOUT)
    put(ch,2,TIMEOUT)
    put(ch,3,TIMEOUT)
    // Get items out
    int u = get(ch,0,TIMEOUT)
    int v = get(ch,0,TIMEOUT)    
    // Check
    assume u == 3
    assume v == 2
    // Put more int
    put(ch,4,TIMEOUT)
    // Get more out
    int w = get(ch,0,TIMEOUT)
    int x = get(ch,0,TIMEOUT)    
    // Check
    assume w == 4
    assume x == 1
    
    
---