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

original.name="Type_Invalid_15"
js.execute.ignore=true
======
>>> main.whiley
type nat is (int x) where x >= 0

type Random is {nat index, nat[] sequence}
// index is valid position in random sequence
where index < |sequence|
// Sequence is valid card index
where all { i in 0..|sequence| | sequence[i] < 52 }

function next(Random r) -> (nat index, Random nr)
ensures index < 52:
    // Get item from random sequence
    int result = r.sequence[r.index]
    // Move to next item
    r.index = r.index + 1
    // Check for overflow
    if r.index == |r.sequence|:
        r.index = 0
    //
    return (nat) result, r

public export method test():
   int item
   Random r = {index:0, sequence:[5,10,2]}
   //
   (item,r) = next(r)
   assume item == 5
   //
   (item,r) = next(r)
   assume item == 10
   //
   (item,r) = next(r)
   assume item == 2
---
E702 main.whiley 14,14:24
E718 main.whiley 14,14:24