Isabelle中LAGC语义的机械化
Mechanization of LAGC Semantics in Isabelle
摘要：
当试图以自动方式验证程序的属性时，形式化的程序设计语言语义是必不可少的。Din等人使用一种新的方法，通过提出一种模块化的跟踪语义来加强对并发程序的推理能力，该语义可以灵活地适应最突出的命令式程序设计语言范例。这些语义通过为个体的局部系统生成抽象的、符号化的轨迹，将局部环境中的评价与全局环境中的评价解耦。然后，这些轨迹被组合和具体化，从而产生全局系统的全局轨迹。因此，这些语义被称为局部抽象，全局具体（LAGC）。在这项工作中，我们提出了一个形式化的LAGC语义流行的定理证明环境Isabelle/HOL。给出的模型是基于Din等人先前关于LAGC语义理论的工作，包括基本定理的形式化、While语言（WL）的LAGC语义以及While语言的扩展版本（WLEXT）的LAGC语义。此外，我们使用我们的伊莎贝尔模型，以提供正式的证明LAGC语义，这还没有在原来的文件中分析的几个先进的性能。虽然工作的主要目标是以数学上严格的方式形式化LAGC语义，但我们也实现了高水平的证明自动化，并设法为程序痕迹的计算提供高效的代码生成。由于语义的形式化是高度模块化的，所给出的理论在将来可以扩展到更复杂的程序设计语言范例。
英文摘要：
Formal programming language semantics are imperative when trying to verify properties of programs in an automated manner. Using a new approach, Din et al. strengthen the ability of reasoning about concurrent programs by proposing a modular trace semantics, which can flexibly adapt to the most prominent imperative programming language paradigms. These semantics decouple the evaluation in the local environments from the evaluation in the global environment by generating abstract, symbolic traces for the individual, local systems. The traces are then composed and concretized, resulting in global traces for the global system. Hence, these semantics are called Locally Abstract, Globally Concrete (LAGC). In this work, we present a formalization of the LAGC semantics in the popular theorem proving environment Isabelle/HOL. The given model is based on the prior work on the theory of LAGC semantics by Din et al. and includes formalizations of the basic theorems, the LAGC semantics for the While Language (WL), as well as the LAGC semantics for an extended version of the While Language (WLEXT). We furthermore use our Isabelle model in order to provide formal proofs for several advanced properties of the LAGC semantics, which have not been analyzed in the original paper. Whilst the main goal of the work was to formalize the LAGC semantics in a mathematically rigorous manner, we also achieve a high level of proof automatization and manage to contribute an efficient code-generation for the computation of program traces. As the formalization of the semantics is highly modular, the given theories could in the future be extended with even more sophisticated programming language paradigms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
