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="RecursiveType_Valid_30"
whiley.compile.ignore=true
WhileyCompiler.issue=936
======
>>> main.whiley
type Tree is null | Node

type Node is {int data, Tree rhs, Tree lhs}
where (lhs is null) || (lhs.data < data)
where (rhs is null) || (rhs.data > data)

function Tree(int data, Tree left, Tree right) -> Tree
requires (left is null) || (left.data < data)
requires (right is null) || (right.data > data):
    return {data: data, rhs: right, lhs: left}

public export method test() :
    Tree l1 = Tree(1, null, null)
    Tree l2 = Tree(3, null, null)
    Tree l3 = Tree(5, null, null)
    Tree t1 = Tree(2, l1, l2)
    assume t1 == {data:2,lhs:{data:1,lhs:null,rhs:null},rhs:{data:3,lhs:null,rhs:null}}
    Tree t2 = Tree(4, t1, l3)
    assume t2 == {data:4,lhs:{data:2,lhs:{data:1,lhs:null,rhs:null},rhs:{data:3,lhs:null,rhs:null}},rhs:{data:5,lhs:null,rhs:null}}
---