一句话：提出 SpecTec DSL 与工具链，将 Wasm 形式规范作为单一事实来源，自动生成规范文档与元级解释器并发现规范错误。
WebAssembly（Wasm）的规范包含完整形式语义，新特性须同时具备形式语义、散文说明和参考解释器，手工维护冗余且易错。本文提出 SpecTec：一种面向 Wasm 规范编写与标准化工件生成的领域特定语言与工具链。SpecTec 作为单一事实来源，可从语义定义生成排版规范（含形式定义与散文伪代码）和元级解释器；测试生成与交互式定理证明后端仍在计划。评估中，SpecTec 可表示最新 Wasm 2.0，生成的元级解释器通过 100% 适用官方测试套件，并发现已修正历史错误及五个候选提案中的十个错误。作者希望 Wasm 标准社区采用 SpecTec 规范未来版本。
WebAssembly (Wasm) is a portable low-level bytecode language and virtual machine that has seen increasing use in a variety of ecosystems. Its specification is unusually rigorous – including a full formal semantics for the language – and every new feature must be specified in this formal semantics, in prose, and in the official reference interpreter before it can be standardized. With the growing size of the language, this manual process with its redundancies has become laborious and error-prone, and in this work, we offer a solution. We present SpecTec, a domain-specific language (DSL) and toolchain that facilitates both the Wasm specification and the generation of artifacts necessary to standardize new features. SpecTec serves as a single source of truth — from a SpecTec definition of the Wasm semantics, we can generate a typeset specification, including formal definitions and prose pseudocode descriptions, and a meta-level interpreter. Further backends for test generation and interactive theorem proving are planned. We evaluate SpecTec’s ability to represent the latest Wasm 2.0 and show that the generated meta-level interpreter passes 100% of the applicable official test suite. We show that SpecTec is highly effective at discovering and preventing errors by detecting historical errors in the specification that have been corrected and ten errors in five proposals ready for inclusion in the next version of Wasm. Our ultimate aim is that SpecTec should be adopted by the Wasm standards community and used to specify future versions of the standard.
@article{YounSLRBGLPRWR24,
title = {Bringing the WebAssembly Standard up to Speed with SpecTec},
author = {Dongjun Youn and Wonho Shin and Jaehyun Lee and Sukyoung Ryu and Joachim Breitner and Philippa Gardner and Sam Lindley and Matija Pretnar and Xiaojia Rao and Conrad Watt and Andreas Rossberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656440}
}