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

original.name="Property_Valid_4"
======
>>> main.whiley
property contains(int[] xs, int x) -> (bool r):
    return some { i in 0..|xs| | xs[i] == x }

function id(int[] xs, int x) -> (int[] ys)
requires contains(xs,x)
ensures contains(ys,x):
    return xs

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


---