 As a tool for investigating program properties, full abstraction can be seen as a completeness property of denotational semantics: every equivalence of programs that can be proved operationally, can also be proved by denotational means. Equivalently, a denotational proof that two terms are not equivalent will be enough to show that they are not interchangeable in every program context.