Implicit heterogeneous metaprogramming (a.k.a. offshoring) is an attractive approach for generating C with some correctness guarantees: generate OCaml code, where the correctness guarantees are easier to establish, and then map that code to C. The key idea is that simple imperative OCaml code looks like a non-standard notation for C. Regretfully, it is false, when it comes to mutable variables. In the past, the approach was salvaged by imposing strong ad hoc restrictions. The present paper for the first time investigates the problem systematically and discovers general solutions needing no restrictions. In the process we explicate the subtleties of modeling mutable variables by values of reference types and arrive at an intuitively and formally clear correspondence. We also explain C assignment without resorting to L-values.
翻译:(a.k.a.离岸外包)是一种具有某种正确性保障的具有吸引力的生成C的诱人方法:生成OCaml代码,其中正确性保障更容易确定,然后将该代码映射到C。 关键的想法是,简单的OCaml代码看起来像C. 可惜的是,当它涉及到变异变量时,它是假的。过去,通过施加严格的临时限制来挽救了这一方法。本文件首次系统地调查了这一问题,发现了不需要限制的一般性解决方案。 在这一过程中,我们通过参考类型的价值来解释模型变异变量的微妙性,并得出直截了当和正式明确的通信。我们还在不使用L值的情况下解释了C的指定。