 What remains to be examined here is the nature of the implementation relation thus defined. Analyzing this relation is essential to define the notion of correctness  (§7).  Indeed, a correct program amounts to a correct implementation of an algorithm; and a correct computing system is a correct implementation of a set of specifications. In other words, under this view, the notion of correctness is paired with that of implementation for any LoA: any level can be said to be correct with respect to upper levels if and only if it is a correct implementation thereof.