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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

original.name="Property_Valid_16"
boogie.ignore=true
======
>>> main.whiley
// This benchmark was created specifically to test recursive
// properties.
type Node is {int data, List next}
type List is null|Node

// A recursive property capturing the concept of
// the sum of a List
property sum(List l, int s) -> (bool r):
    return (l is Node && sum(l.next, s - l.data)) ||
           (l is null && s == 0)

// Another recursive property capturing the different in length
// between the head of a list and a given position within that
// list.
property diff(List head, List pos, int d) -> (bool r):
    return (head == pos && d == 0) ||
           (head is Node && diff(head.next, pos, d - head.data))

function sum(List l) -> (int r)
// Ensure we capture the real length
ensures sum(l,r):
    //
    int x = 0
    List ol = l // ghost
    // iterate until 
    while l is Node
    where diff(ol,l,x):
        x = x + l.data
        l = l.next
    //
    return x

public export method test():
    // List of length 1
    List l1 = {data: 0, next: null}
    // List of length 2
    List l2 = {data: 1, next: l1}
    // List of length 3
    List l3 = {data: 2, next: l2}
    //
    assert sum(null) == 0
    //
    assert sum(l1) == 0
    //
    assert sum(l2) == 1
    //
    assert sum(l3) == 3    
---