AI 中文总结
该研究提出P4-SpecTec，将语言机械化框架应用于P4，通过算法推理规则实现可执行的P4语义，发现24个错误，其被有条件采用为P4官方规范创作工具链。
AI 中文摘要
编程语言会不断演进，但往往缺乏完整且无歧义的语法和语义定义。歧义与不一致性会悄然进入规范，表现为构成语言生态系统的规范、实现和形式化之间的分歧。即使存在规范性规范，要保持生态系统同步也是一项艰巨任务。语言机械化框架通过将机械化规范作为唯一真实来源，从中生成实现和文档，解决了这一问题。最近，该方法已分别通过ESMeta和Wasm-SpecTec集成到JavaScript和WebAssembly（Wasm）的实际规范中。尽管取得了这些成功，但如何将ESMeta和Wasm-SpecTec推广到其他语言规范仍是一个悬而未决的问题。作为解决该问题的第一步，我们提出了P4-SpecTec，这是一个用于P4编程语言的语言机械化框架，作为语言机械化实际应用的案例研究。P4带来了独特的挑战，特别是其类型系统机械化需具备可执行性，而ESMeta和Wasm-SpecTec均不支持这一点。为应对这一挑战，我们引入算法推理规则作为机械化的主要工具，使机械化的P4静态语义和动态语义可分别作为P4类型检查器和解释器执行。我们对最新的P4规范进行了机械化，并利用其可执行性，在官方P4规范和参考编译器中发现了24个错误。此外，P4-SpecTec将规范文档生成为算法散文形式，使其对P4开发者而言易于理解。P4-SpecTec被有条件地采用为官方P4规范创作工具链。
英文摘要
Programming languages evolve, but often without a complete and unambiguous definition of their syntax and semantics. Ambiguities and inconsistencies are silently introduced into specifications, and manifest as divergences between the specification, implementations, and formalizations that constitute the language ecosystem. Even in rare cases when a normative specification exists, keeping the ecosystem in sync is a daunting task. Language mechanization frameworks address this problem by treating a mechanized specification as the single source of truth, from which implementations and documents are generated. Recently, this approach has been integrated into the actual JavaScript and WebAssembly (Wasm) specifications with ESMeta and Wasm-SpecTec, respectively. Despite these successes, it remains an open question how to extrapolate ESMeta and Wasm-SpecTec to other language specifications. As a first step towards addressing this question, we present P4-SpecTec, a language mechanization framework for the P4 programming language, as a case study of real-world adoption of language mechanization. P4 introduces unique challenges, in particular the requirement that its type system mechanization should be executable, which is not supported by either ESMeta or Wasm-SpecTec. To address this challenge, we introduce algorithmic inference rules as the primary instrument for mechanization, enabling the mechanized P4 static and dynamic semantics to be executed as a P4 type checker and interpreter, respectively. We mechanized the most recent P4 specification, and utilizing its executability, identified 24 bugs across the official P4 specification and the reference compiler. Furthermore, P4-SpecTec derives a specification document as prose algorithms, making it accessible to P4 developers. P4-SpecTec is conditionally adopted as the official P4 specification authoring toolchain.
