LSeg

leg.sil

field next: Ref
field value: Int

predicate lseg(this: Ref, end: Ref) {
    acc(this.value, write) && acc(this.next, write) &&
       (this.next != end ==> this.next != null && acc(lseg(this.next, end), write))
}

function get(this: Ref, i: Int, end: Ref): Int
    requires acc(lseg(this, end), write)
    requires 0 <= i && i < length(this, end)
{
    unfolding acc(lseg(this, end), write) in (i == 0 ? this.value : get(this.next, i-1, end))
}

function length(this: Ref, end: Ref): Int
    requires acc(lseg(this, end), write)
    ensures result > 0
{
    unfolding acc(lseg(this, end), write) in (this.next == end ? 1 : 1 + length(this.next, end))
}

method init(this: Ref, val: Int)
    requires acc(this.next, write)
    requires acc(this.value, write)
    ensures acc(lseg(this, null), write)
    ensures length(this, null) == 1
    ensures get(this, 0, null) == val
{
    this.next := null
    this.value := val
    fold acc(lseg(this, null), write)
}