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:
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.
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().
Let us put this in contrast with the function NewBad:
The contract is bad in a number of ways:
- The field
nextis 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
ListAPI. - 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.
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