K —A Semantic Framework for Programming Languages and Formal Analysis
K —A Semantic Framework for Programming Languages and Formal Analysis
复制标题
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Xiaohong Chen;Grigore Ro¸su
中科院分区：
文献类型：
--
作者：
Xiaohong Chen;Grigore Ro¸su
.我们给出了一个概述的应用和基础的K语言框架，一个语义框架的编程语言和形式化分析工具。K代表了20年来追求理想语言框架愿景的努力，编程语言必须有正式的定义，以及给定语言的工具，如解析器，解释器，编译器，基于语义的调试器，状态空间探索器，模型检查器，演绎程序验证器等。可以从语言的一个可执行的参考形式定义中导出，并且不需要相同语言的其他语义。语言工具的正确性由证明对象逐个保证，证明对象将严格的数学证明编码为工具执行的每个任务的证书，并且可以由第三方证明检查器进行机械检查。
. We give an overview on the applications and foundations of the K language framework, a semantic framework for programming languages and formal analysis tools. K represents a 20-year effort in pursuing the ideal language framework vision, where programming languages must have formal definitions, and tools for a given language, such as parsers, interpreters, compilers, semantic-based debuggers, state-space explorers, model checkers, deductive program verifiers, etc., can be derived from just one reference formal definition of the language, which is executable, and no other semantics for the same language should be needed. The correctness of the language tools is guaranteed on a case-by-case basis by proof objects, which encode rigorous mathematical proofs as certificates for every individual task that the tools do and can be mechanically checked by third-party proof checkers.