original.name="Property_Valid_15"
======
>>> 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 length of a List
property length(List l, int len) -> (bool r):
    return (l is Node && length(l.next,len-1)) ||
           (l is null && len == 0)

function len(List l) -> (int r)
// Ensure we capture the real length
ensures length(l,r):
    //
    if l is null:
        return 0
    else:
        return len(l.next) + 1

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