Computational adequacy

Of course, one expects the operational and the denotational semantics to match. This property is known as computational adequacy. If computational adequacy holds, one can develop correct programs using algebra and analysis, completely ignoring the details of the operational semantics. (Of course, in order to obtain efficient programs, some aspects of the operational semantics will have to be taken into account. But, again, for such purposes, it is often sufficient to consider abstractions of the operational semantics.)