Predicates
Predicates abstract over assertions, i.e., giving a name to a parametrized assertion. Predicates can be used for representing 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 to denote 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 list1.
We will implement the following public API for the construction and manipulation of lists:
In a first step, we focus only on specifying memory access. Then in the second step, the contracts are completed for functional correctness. The following client code will be verified in the final example:
Declaring predicates
Here we define the predicate elements to represent access to all elements in a list l:
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 not only to acc(&l.Value) && acc(&l.next), but also 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 exhaled and we may no longer access l.Value:
ERROR Assignment might fail.
Permission to l.Value might not suffice.
Folding fails if the assertion from the body does not hold:
ERROR Fold might fail.
Permission to elements(l.next) might not suffice.
We can fix this by requiring elements(tail) if tail != nil.
Unwrapping predicate instances with unfold
The unfold statement exchanges a predicate instance with its body.
Unfolding fails, if the predicate instance is not held.
If we try to unfold elements(l) twice, the second statement causes an 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.
To recover the concrete permissions, we unfold the predicates in the reverse order.
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
foldstatement exchanges the body of a predicate for a predicate instance. If the assertion in the body does not hold, an error is reported.The
unfoldstatement exchanges a predicate instance with its body. If the predicate instance is not held, an error is reported.
Go's standard library comes with a doubly linked list. While it has been verified (Verifying Go’s Standard Library (Jenny)), we use a much simpler API for our exposition.