Abstracting memory access with predicates

In this section, we emphasize how predicates can abstract memory access, and help enforce the information hiding principle, hiding implementation details such as non-exported fields, memory layout, or other internal assumptions.

The core idea is that clients shall only need to hold predicate instances, allowing them to interact with an API without exposing specific permissions to fields. We exemplify this on a subset of the List API, for now focusing only on specifying memory access without proving functional correctness.

Previously, we defined the predicate elements:

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

Predicates can be defined with a receiver, too. This conveniently couples the predicate to the type. As a convention, we choose the name Mem to signal that this predicate abstracts the memory.

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

/*@
// Represents access to the List element and all elements in its tail.
pred (l *List) Mem() {
	l != nil ==> (acc(l) && l.next.Mem())
}
@*/

Note the slight difference: for l.Mem(), l could be nil whereas elements(l) implies l != nil.

A predicate instance l.Mem() can be obtained, for example, by allocating a new list. The postconditions of Empty and New ensure this. For New, the contract in turn requires holding tail.Mem().

// Returns the empty list.
// @ ensures l.Mem()
// @ ensures l.IsEmpty()
func Empty() (l *List) {
	l = (*List)(nil)
	// @ fold l.Mem()
	return
}

// New creates a new List node with the specified value and tail.
// @ requires tail.Mem()
// @ ensures out.Mem()
// @ ensures !out.IsEmpty()
// @ ensures out.Head() == value
func New(value int, tail *List) (out *List) {
	out = &List{next: tail, Value: value}
	// @ fold out.Mem()
	return
}

Let us put this in contrast with the function NewBad:

// @ ensures acc(&out.Value) && acc(&out.next)
// @ ensures out.next == tail
// @ ensures out.Value == value
func NewBad(value int, tail *List) (out *List) {
	out = &List{next: tail, Value: value}
	return
}

The contract is bad in a number of ways:

• The field next is used in the contract although it is non-exported and clients of the package are not even aware of its existence.
• Internal decisions are leaked, such as using a linked list to provide the List API.
• When the implementation is changed, the contract would need to get changed as well, breaking the API.

Hiding implementation details

Another internal decision is the encoding of the empty list. In this example, we implement it as (*List)(nil). While this is an idiomatic choice in Go, we still exemplify how this can be hidden. Some functions like Head cannot be called with an empty list. The precondition l != nil would leak this to clients. Instead, we provide a pure method IsEmpty to be used in contracts.

// Returns the empty list.
// @ ensures l.Mem()
// @ ensures l.IsEmpty()
func Empty() (l *List) {
	l = (*List)(nil)
	// @ fold l.Mem()
	return
}

// Returns true iff the list is empty.
// @ pure
// @ requires l.Mem()
// @ decreases
func (l *List) IsEmpty() (empty bool) {
	return l == nil
}

// Head returns the value of the first element in the list.
// @ pure
// @ requires l.Mem()
// @ requires !l.IsEmpty()
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding l.Mem() in @*/ l.Value
}

func client() {
	e := Empty()
	// @ assert e.Mem()
	// @ assert e.IsEmpty()
	l1 := New(11, e)
	// @ assert l1.Mem()
	// @ assert l1.Head() == 11
	l2 := New(22, Empty())
	// @ assert l2.Head() == 22
	l3 := New(33, l2)
	// @ assert l3.Head() == 33
}

Note that we implement Mem such that it holds for the empty list as well. This enables us to call methods such as e.IsEmpty() on it.

List example so far

package list

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


/*@
// Represents access to the List element and all elements in its tail.
pred (l *List) Mem() {
	l != nil ==> (acc(l) && l.next.Mem())
}
@*/

// Returns the empty list.
// @ ensures l.Mem()
// @ ensures l.IsEmpty()
func Empty() (l *List) {
	l = (*List)(nil)
	// @ fold l.Mem()
	return
}


// New creates a new List node with the specified value and tail.
// @ requires tail.Mem()
// @ ensures out.Mem()
// @ ensures !out.IsEmpty()
// @ ensures out.Head() == value
func New(value int, tail *List) (out *List) {
	out = &List{next: tail, Value: value}
	// @ fold out.Mem()
	return
}


// Head returns the value of the first element in the list.
// @ pure
// @ requires l.Mem()
// @ requires !l.IsEmpty()
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding l.Mem() in @*/ l.Value
}


// Returns true iff the list is empty.
// @ pure
// @ requires l.Mem()
// @ decreases
func (l *List) IsEmpty() (empty bool) {
	return l == nil
}


func client() {
	e := Empty()
	// @ assert e.Mem()
	// @ assert e.IsEmpty()
	l1 := New(11, e)
	// @ assert l1.Mem()
	// @ assert l1.Head() == 11
	l2 := New(22, Empty())
	// @ assert l2.Head() == 22
	l3 := New(33, l2)
	// @ assert l3.Head() == 33
}