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 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, focusing only on specifying memory access without proving functional correctness for now.

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 several ways:

• The field next is used in the contract, although it is non-exported, and the package's clients are unaware 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 also needs to get changed, 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 so that it also holds for the empty list. 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
}