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="Old_Valid_17"
js.compile.ignore=true
boogie.ignore=true
Whiley2Boogie.issue=128
======
>>> main.whiley
type List is null|Node
type Node is &{ List next }

variant unchanged(List l)
where (l is Node) ==> (l->next == old(l->next))
where (l is Node) ==> unchanged(l->next)

method m(List l)
ensures unchanged(l):
    skip

public export method test():
    List l1 = new {next:null}
    List l2 = new {next:l1}
    //
    m(l2)
    assert l2->next == l1
    assert l1->next == null
---