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

original.name="While_Valid_52"
======
>>> main.whiley
function sum(int[] xs) -> (int r)
// Every element in xs is non-negative
requires all { i in 0..|xs| | xs[i] >= 0 }
// Every element in xs is actually positive
requires all { i in 0..|xs| | xs[i] > 0 }
// result is positive
ensures r >= 0:
    //
    int i = 0
    int sum = 0
    //
    while i < |xs|
    where i >= 0 && sum >= 0:
        sum = sum + xs[i]
        i = i + 1
    //
    return sum

public export method test():
    assume sum([1;0]) == 0
    assume sum([1,2,3]) == 6
---