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 shall 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 refer the reader to the mathematical types reference if questions arise.

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

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

In the table, we give 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.