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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129

original.name="Complex_Valid_11"
======
>>> main.whiley
// This is cut-down version of the full card benchmark.  This is to
// test the basic machinery without the associated performance problems.
type nat is (int x) where x >= 0

// =======================================
// Card Definition
// =======================================

// Suites
final int HEARTS = 1
final int CLUBS = 2

// Ordinals
final int TWO = 2
final int THREE = 3
final int FOUR = 4

type Card is { int suite, int ordinal }
// Suite between hearts and clubs
where HEARTS <= suite && suite <= CLUBS
// Ordinal between 2 and ACE (high)
where 2 <= ordinal && ordinal <= FOUR

// =======================================
// Card Constants
// =======================================

final Card TWO_HEARTS = { suite: HEARTS, ordinal: TWO }
final Card THREE_HEARTS = { suite: HEARTS, ordinal: THREE }
final Card FOUR_HEARTS = { suite: HEARTS, ordinal: FOUR }

final Card TWO_CLUBS = { suite: CLUBS, ordinal: TWO }
final Card THREE_CLUBS = { suite: CLUBS, ordinal: THREE }
final Card FOUR_CLUBS = { suite: CLUBS, ordinal: FOUR }

// =======================================
// DECK
// =======================================

type Deck is (Card[] cards)
// Exactly 6 cards in a deck
where |cards| == 6

// A real test of verifier performance!!
final Deck deck = [
        // Hearts
        TWO_HEARTS,
        THREE_HEARTS,
        FOUR_HEARTS,
        // Clubs
        TWO_CLUBS,
        THREE_CLUBS,
        FOUR_CLUBS
    ]

// =======================================
// RANDOM
// =======================================
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] < 6 }

function Random(nat[] sequence) -> Random
requires |sequence| > 0
requires all { i in 0..|sequence| | sequence[i] < 6 }:
    //
    return { index: 0, sequence: sequence }

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

// =======================================
// SHUFFLE
// =======================================

function swap(Deck deck, nat from, nat to) -> Deck
requires from < 6 && to < 6:
    // Swap two cards around
    Card tmp = deck[from]
    deck[from] = deck[to]
    deck[to] = tmp
    //
    return deck

// "Randomly" shuffle the deck
function shuffle(Deck deck, Random rand, nat count) -> Deck:
    //
    nat i = 0
    //
    while i < count:
       nat from
       nat to  
       (from,rand) = next(rand)
       (to,rand) = next(rand)
       deck = swap(deck,from,to)
       i = i + 1
    //
    return deck
    
// =======================================
// TEST
// =======================================

public export method test():
    // Not a very long "random" sequence
    Random rand = Random([3,4,2,5,1,2])
    // Shuffle the deck ten times
    Deck d = shuffle(deck,rand,10)
    //
    assert |d| == 6


---