Predicates

Predicates abstract over assertions, i.e., giving a name to a parametrized assertion. Predicates can represent memory access to data structures of possibly unbounded size, such as linked lists or binary trees. While quantified permissions are often used to specify pointwise access, e.g., to elements of a slice, predicates are suitable for denoting access to recursive data structures.

Running example: List

Throughout the sections of this chapter, we will follow the example of a List data structure for storing integer values, implemented as a singly linked list¹.

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value int
}

We will implement the following public API for the construction and manipulation of lists:

// Returns the empty list.
func Empty() (l *List)

// New creates a new List node with the specified value and tail.
func New(value int, tail *List) (out *List)

// Tail returns a new list that is the tail of the original list,
// excluding the first element.
func (l *List) Tail() (out *List)

// Remove returns the list with the element at index i deleted.
func (l *List) Remove(i int) (out *List)

// Head returns the value of the first element in the list.
func (l *List) Head() (value int)

// Get returns the element at index i in the list.
func (l *List) Get(i int) (value int)

// Returns true iff the list is empty.
func (l *List) IsEmpty() (empty bool) {

// Returns the length of the list.
func (l *List) Length() (length int)

In a first step, we focus only on specifying memory access. Then, the contracts are completed for functional correctness in the second step. The following client code will be verified in the final example:

func client() {
	ll := Empty()
	l0 := ll.Length()
	// @ assert l0 == 0
	ll = New(11, ll)
	// @ assert ll.Mem()
	// @ assert ll.Head() == 11
	// @ assert ll.View() == seq[int]{11}
	l1 := ll.Length()
	// @ assert l1 == 1
	ll = ll.Tail()
	// @ assert ll.View() == seq[int]{}
	ll = New(22, Empty())
	// @ assert ll.Head() == 22
	ll = New(33, ll)
	// @ assert ll.Head() == 33
	l2 := ll.Length()
	// @ assert l2 == 2
	v0 := ll.Get(0)
	v1 := ll.Get(1)
	// @ assert v0 == 33
	// @ assert v1 == 22
	ll := ll.Remove(1)
	l3 := ll.Length()
	// @ assert ll.Head() == 33
	// @ assert l3 == 1
}

Declaring predicates

Here, we define the predicate elements to represent access to all elements in a list l:

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value int
}


/*@
pred elements(l *List) {
	acc(&l.Value) && acc(&l.next) && (l.next != nil ==> elements(l.next))
}
@*/

Predicates are defined with the keyword pred and possibly with parameters. The body is a single self-framing assertion.

Note that elements is recursive and represents access to acc(&l.Value) && acc(&l.next) and to the elements in its tail.

A predicate instance is not equivalent to its body and we must explicitly exchange between the two with the fold and unfold statements, which we study next.

Creating predicate instances with fold

The fold statement exchanges the body of a predicate for a predicate instance. In the following example, we allocate a new list and highlight with asserts that the assertion from the body of elements holds for l. With the statement fold elements(l), we exchange these for the predicate instance elements(l) as a token representing access to the list. However, acc(&l.Value) has been exhale, and and we may no longer access l.Value:

	l := &List{Value: 1, next: nil}
	// @ assert acc(&l.Value) && acc(&l.next) && l.next == nil
	// @ assert acc(&l.Value) && acc(&l.next) && (l.next != nil ==> elements(l.next))

	// @ fold elements(l)

	// @ assert elements(l)

	v := l.Value // error

ERROR Assignment might fail. 
Permission to l.Value might not suffice.

Folding fails if the assertion from the body does not hold:

// @ ensures elements(l)
func newFail(value int, tail *List) (l *List) {
	l := &List{Value: value, next: tail}
	// @ fold elements(l) // error
	return l
}

ERROR Fold might fail. 
Permission to elements(l.next) might not suffice.

We can fix this by requiring elements(tail) if tail != nil.

// @ requires tail != nil ==> elements(tail)
// @ ensures elements(l)
func newList(value int, tail *List) (l *List) {
	l := &List{Value: value, next: tail}
	// @ fold elements(l)
	return l
}

Unwrapping predicate instances with unfold

The unfold statement exchanges a predicate instance with its body.

	l := &List{Value: 1, next: nil}
	// @ fold elements(l)
	// @ assert elements(l)
	// @ unfold elements(l)
	// @ assert acc(&l.Value) && acc(&l.next) && (l.next != nil ==> elements(l.next))
	v := l.Value

Unfolding fails, if the predicate instance is not held. If we try to unfold elements(l) twice, the second statement causes an error:

	l := &List{Value: 1, next: nil}
	// @ fold elements(l)
	// @ unfold elements(l)
	// @ unfold elements(l) // error

ERROR Unfold might fail. 
Permission to elements(l) might not suffice.

Recursive predicates

Predicates can be recursive, as seen with elements. In the following example, we build a list with 3 elements, always folding the permissions. elements(l3) abstracts access to the full list and has the predicate instances elements(l2) and elements(l1) folded within it. We could continue this process and handle a list of possibly unbounded size. We unfold the predicates in the reverse order to recover the concrete permissions.

	l1 := &List{Value: 1, next: nil}
	// @ fold elements(l1)
	l2 := &List{Value: 2, next: l1}
	// @ fold elements(l2)
	l3 := &List{Value: 3, next: l2}
	// @ fold elements(l3)
	s := 0
	l := l3
	// @ assert elements(l)
	// @ invariant l != nil ==> elements(l)
	for l != nil {
		// @ unfold elements(l)
		s += l.Value
		l = l.next
	}

Please note that we lose access when traversing the list to sum the elements, which is undesirable.

Summary

Predicates abstract over assertions, i.e., giving a name to a parametrized assertion.

The fold statement exchanges the body of a predicate for a predicate instance. If the assertion in the body does not hold, an error is reported.

The unfold statement exchanges a predicate instance with its body. If the predicate instance is not held, an error is reported.