An Example for Metamodeling Syntax and Semantics of Two Languages, their Transformation, and a Correctness Criterion