Predicates as termination measures

Predicate instances can be used as termination measures. The measure decreases if an instance is nested within another predicate instance. For example, l1.Mem() is nested within l2.Mem() and l2.Mem() is nested within l3.Mem().

l1 := New(1, Empty())
// @ fold l1.Mem()
l2 := New(2, l1)
// @ fold l2.Mem()
l3 := New(3, l2)
// @ fold l3.Mem()

The termination measure is lower bounded for predicate instances with a finite unfolding ¹. For example, l3.Mem() has two predicate instances nested within, whereas l1.Mem() has no other predicate instance nested within.

To prove the termination of the List method Length, we add the termination measure l.Mem(). As is common for recursive functions, we unfold the predicate instance before the recursive call. It is decreasing since l.next.Mem() is nested within l.Mem().

// Returns the length of the list.
// @ preserves acc(l.Mem(), 1/2)
// @ ensures length == len(l.View())
// @ decreases l.Mem()
func (l *List) Length() (length int) {
	if l == nil {
		return 0
	} else {
		// @ unfold acc(l.Mem(), 1/2)
		length = 1 + l.next.Length()
		// @ fold acc(l.Mem(), 1/2)
		return length
	}
}

Please note that we write decreases l.Mem() instead of decreases acc(l.Mem(), 1/2), even if we only require acc(l.Mem(), 1/2).

For the List API, we can use the termination measure l.Mem() for the methods Length, Get, and View.

Using the length of a List or the sequence length from the abstraction function View might be tempting as an integer termination measure. For this, the function must be pure, which requires a termination measure in turn.

We chose a recursive implementation for Length to preserve access to l.Mem(). An idiomatic iterative implementation is more challenging to verify. When iteratively iterating over a list, we keep unfolding current.Mem() and lose access to the elements already visited. It is not immediately clear how to fold the predicate instances back such that l.Mem() is preserved by LengthIterative. A common approach is defining a predicate that denotes access to a list segment instead of the entire tail. Alternatively, magic wands are applicable in this situation.

// @ requires l.Mem()
// @ decreases l.Mem()
func (l *List) LengthIterative() (length int) {
	current := l
	// @ invariant current.Mem()
	// @ decreases current.Mem()
	for current != nil {
		// @ unfold current.Mem()
		length += 1
		current = current.next
	}
	return
}

/*@
pred stream(l *List) {
	acc(l) && stream(l.next)
}
@*/

// @ requires stream(l)
// @ decreases
func streaming(l *List) {
	a := 0
	// @ invariant stream(l)
	// @ decreases stream(l)
	for {
		// @ unfold stream(l)
		a += l.Value
		l = l.next
	}
}