We prove the correctness of a translation from while programs with
  parameterless procedures into an abstract machine code with emphasis
  on the implementation of control structures by jumps. The presented
  proof is based on a denotational semantics for the source and a
  denotational characterization of the operational semantics for the
  target language, both given as predicate transformers working on a
  common state space. This enables us to perform the actual
  compiler-correctness proof elegantly in the framework of complete
  lattices.

  At this our main interest lies on the preservation of partial
  correctness since this is -- in our opinion -- the more manageable
  correctness concept for realistic compilers and real machines, which
  is exactly the goal of the Verifix-project.