We investigate methods and tools to analyze translations
between programming languages with respect to
observational semantics.
We consider a framework where the behavior of programs is
observed by (possibly multiple) convergence predicates in arbitrary
contexts.
While observational correctness is taken to be the fundamental
notion of correctness of a translation, we emphasize the role of other correctness conditions like
adequacy and full abstraction of translations.
As a tool for proving these correctness properties, we propose a notion of
convergence equivalence as a means
for proving adequacy for compositional translations which
avoids explicit reasoning about
contexts.
Revised and expanded version of IFIP TCS paper.