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

original.name="TypeEquals_Valid_59"
whiley.compile.ignore=true
WhileyCompiler.issue=1003
======
>>> main.whiley
type nat is (int n) where n >= 0

function f(int|int[]|(int|null)[] x) -> (int r)
ensures (x is int[] && |x| > 0) ==> (r == x[0]):
    //
    if x is int[] && |x| > 0:
        return x[0]
    else:
        return 0

public export method test():
    //
    (int|null)[] a1 = [123]
    (int|null)[] a2 = [null]
    int[] a3 = [124]
    //
    assert f(a1) == 123
    assert f(a2) == 0
    assert f(a3) == 124
    assert f(0) == 0
    //
---