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

original.name="Quantifiers_Valid_4"
======
>>> main.whiley
// This is something of a verifier workout.  Its trying to trigger a
// matching loop.
property equals(int[] xs, int[] ys) -> (bool r):
   return |xs| == |ys| && all { i in 0..|xs| | xs[i] == ys[i] }

property sorted_a(int[] xs) -> (bool r):
   return |xs| == 0 || all { i in 1 .. |xs| | xs[i-1] < xs[i] }

property sorted_b(int[] xs) -> (bool r):
   return |xs| == 0 || all { i in 0 .. |xs|-1 | xs[i] < xs[i+1] }

property consecutive_a(int[] xs) -> (bool r):
   return |xs| == 0 || all { i in 1 .. |xs| | xs[i-1] + 1 == xs[i] }

property consecutive_b(int[] xs) -> (bool r):
   return |xs| == 0 || all { i in 0 .. |xs|-1 | xs[i] + 1 == xs[i+1] }

function f1(int[] xs) -> (int[] ys)
requires sorted_a(xs)
ensures sorted_a(ys):
    return xs

function f2(int[] xs) -> (int[] ys)
requires sorted_a(xs)
ensures sorted_b(ys):
    return xs

function f3(int[] xs) -> (int[] ys)
requires sorted_b(xs)
ensures sorted_a(ys):
    return xs

function f4(int[] xs) -> (int[] ys)
requires sorted_b(xs)
ensures sorted_b(ys):
    return xs

function g1(int[] xs) -> (int[] ys)
requires consecutive_a(xs)
ensures consecutive_a(ys):
    return xs

function g2(int[] xs) -> (int[] ys)
requires consecutive_a(xs)
ensures consecutive_b(ys):
    return xs

function g3(int[] xs) -> (int[] ys)
requires consecutive_b(xs)
ensures consecutive_a(ys):
    return xs

function g4(int[] xs) -> (int[] ys)
requires consecutive_b(xs)
ensures consecutive_b(ys):
    return xs

function h1(int[] xs) -> (int[] ys)
requires consecutive_a(xs)
ensures sorted_a(ys):
    return xs

function h2(int[] xs) -> (int[] ys)
requires consecutive_b(xs)
ensures sorted_a(ys):
    return xs

function h3(int[] xs) -> (int[] ys)
requires consecutive_a(xs)
ensures sorted_b(ys):
    return xs

function h4(int[] xs) -> (int[] ys)
requires consecutive_b(xs)
ensures sorted_b(ys):
    return xs

method test(int[] xs)
// All indices must match contents
requires all { i in 0..|xs| | xs[i] == i }:
    int[] ys
    //
    assert sorted_a(f1(xs))
    assert sorted_a(f2(xs))
    assert sorted_a(f3(xs))
    assert sorted_a(f4(xs))
    //
    assert sorted_a(g1(xs))
    assert sorted_a(g2(xs))
    assert sorted_a(g3(xs))
    assert sorted_a(g4(xs))
    //
    assert sorted_a(h1(xs))
    assert sorted_a(h2(xs))
    assert sorted_a(h3(xs))
    assert sorted_a(h4(xs))

public export method test():
    test([])
    test([0])
    test([0,1])
    test([0,1,2])
    test([0,1,2,3])
    test([0,1,2,3,4])
    test([0,1,2,3,4,5])
    test([0,1,2,3,4,5,6])

---