理解Lua的垃圾回收--迈向形式化的静态分析器
Understanding Lua's Garbage Collection -- Towards a Formalized Static Analyzer
摘要：
我们为Lua程序设计语言提供了垃圾回收（GC）的语义。有趣的是包含了终结器（类似于面向对象语言中的析构函数）和弱表（弱引用的一种特殊实现）。该模型表达了与GC相关的几个方面，这些方面在Lua的文档中没有涉及，但却影响了程序的可观察行为。我们的模型是机械化的，可以用真实的程序进行测试。我们的长期目标是提供一个正式的Lua程序静态分析器来检测潜在的危险。作为第一步，我们提供了一个原型工具LuaSafe，它可以对程序进行类型转换，以确保它们的行为不受GC的影响。我们的GC模型在实践中通过实验与其机械化进行了验证，并在理论上证明了几个健全的性质。
英文摘要：
We provide the semantics of garbage collection (GC) for the Lua programming language. Of interest are the inclusion of finalizers(akin to destructors in object-oriented languages) and weak tables (a particular implementation of weak references). The model expresses several aspects relevant to GC that are not covered in Lua's documentation but that, nevertheless, affect the observable behavior of programs. Our model is mechanized and can be tested with real programs. Our long-term goal is to provide a formalized static analyzer of Lua programs to detect potential dangers. As a first step, we provide a prototype tool, LuaSafe, that typechecks programs to ensure their behavior is not affected by GC. Our model of GC is validated in practice by the experimentation with its mechanization, and in theory by proving several soundness properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
