编译器中的成本注释认证
摘要：使用所谓的标注方法，将执行成本的信息从目标代码提升到源代码的成本注释上。我们需要明确和灵活的认识以下几个问题：（i）成本注释的含义，（ii）证明它们正确和精确的方法，以及（iii）这些证明如何组合。我们提出了一个所谓的标注方法来解决这三个问题。作为第一步，我们将其应用于一个玩具编译器。这个形式化的研究表明，标注方法具有良好的组合性和可扩展性。为了进一步证明这一观点，我们报告了我们在OCAML编写的原型编译器上实施和测试标注方法的成功经验，这个编译器可以处理C语言的一个大片段。
作者：Roberto M. Amadio (PPS), Nicolas Ayache (PPS, INRIA Paris - Rocquencourt), Yann R''egis-Gianas (PPS, INRIA Paris - Rocquencourt), Ronan Saillard (PPS, INRIA Paris - Rocquencourt)
论文ID：1010.1697
分类：Programming Languages
分类简称：cs.PL
提交时间：2010-10-11