original.name="Reference_Valid_42"
js.compile.ignore=true
boogie.ignore=true
======
>>> main.whiley
type Node is &{ int data, LinkedList next }
type LinkedList is null | Node

property acyclic(LinkedList l) -> (bool r):
    return l is null || acyclic(l->next)

variant unchanged(LinkedList l)
where l is null || *l == old(*l)
where l is null || unchanged(l->next)

method cons(int item, LinkedList head) -> (Node r)
// Incoming list must be acyclic
requires acyclic(head)
// Outgoing list still acyclic
ensures acyclic(r)
// Implemented cons
ensures (r->data == item) && (r->next == head)
// Nothing else changed!
ensures unchanged(head):
    // Allocate fresh node
    return new { data: item, next: head }

public export method test():
    LinkedList l0 = null
    LinkedList l1 = cons(1,l0)
    assert l1->data == 1
    LinkedList l2 = cons(2,l1)
    assert l1->data == 1
    assert l2->data == 2
    assert l2->next == l1

---