机构名称：
¥ 2.0
WebAssembly（WASM）是一种便携式低级字节码语言和虚拟机，在各种生态系统中的使用越来越多。其规范非常严格 - 包括语言的完整正式语义 - 并且必须在本式语义，散文和官方参考解释器中指定每个新功能，然后才能进行标准化。随着语言规模不断增长，这种手动过程及其冗余已变得艰巨且容易出错，在这项工作中，我们提供了一种解决方案。我们提出Spectec，一种特定于领域的语言（DSL）和工具链，可促进WASM规范和标准化新功能所需的工件的产生。Spectec是真理的单一来源 - 从wastm语义的观点定义来看，我们可以生成字体规范，包括正式的定义和散文伪代码描述以及元级解释器。计划了进一步的测试生成和交互式定理的后端。我们评估了Spectec代表最新WASM 2.0的能力，并表明生成的元级口译员通过了适用的官方测试套件的100％。我们表明，Spectec通过检测已纠正的规范中的历史错误以及在五个建议中的五个提案中的十个错误来发现和预防错误非常有效。我们的最终目的是，Spectec应由WASM标准社区采用，并用于指定标准的未来版本。
将WebAssembly标准标准加速使用Spectec
主要关键词
相关文件推荐
