Abstraction functions

An idiomatic verification pattern is to map structures to their essential representation with an abstraction function. One way to specify functional correctness is by describing the effect of functions or methods on the abstract representation. For the abstract representation, we use mathematical types, i.e., ghost types representing mathematical objects, such as sequences or sets. For example, if we were to design a Set data structure, adding an element to a concrete Set would have the same effect as the operation on an abstract, mathematical set.

Abstraction function for List

So far, our contracts for List were concerned with memory access. Now, we want to complete them with functional correctness requirements.

The essence of a List is captured by a sequence. We will not fully introduce sequences at this point, but if questions arise, we will refer the reader to the mathematical types reference.

A sequence of integers seq[int] is constructed recursively from the list, concatenating (++) the sequences. By convention, the abstraction function is called View. Note that the function must be pure, as we want to use it in specifications.

/*@
ghost
pure
requires acc(l.Mem(), 1/2)
decreases l.Mem()
func (l *List) View() seq[int] {
	return l == nil ? seq[int]{} : unfolding acc(l.Mem(), 1/2) in seq[int]{l.Value} ++ l.next.View()
}
@*/

Functional correctness for List

We can specify the functional behavior of the List API methods on the abstract object. For example, New corresponds to concatenating a single element to a sequence.

The table below gives the preconditions and postconditions we add to the contracts. The abstraction function is heap-dependent, and we can evaluate it in the old state to get the original representation. For example, the method Get must return the ith element of the sequence corresponding to the list old(l.View()[i]) index the index is within bounds ( 0 <= i && i < len(l.View())).

The full example can be found here: full linked list example.