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 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, View.

It might be tempting to use the length of a List or the length of the sequence from the abstraction function View 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, in order 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 already visited elements. It is not directly clear how one could fold the predicate instances back such that l.Mem() is preserved by LengthIterative. A common approach is to define a predicate that denotes access to a segment of a list 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
	}
}