C语言Clight子集的机械化语义
Mechanized semantics for the Clight subset of the C language
摘要：
本文介绍了C语言的一个大子集Clight的形式语义。Clight包括指针算术、“struct”和“union”类型、C循环和结构化“switch”语句。Clight是CompCert验证编译器的源语言。Clight的形式语义是一个大步骤的操作语义，它观察终止和发散执行，并产生输入/输出事件的跟踪。Clight的形式语义是使用Coq证明助手机械化的。除了Clight的语义之外，本文还描述了它在CompCert验证编译器中的集成以及验证语义的几种方法。
英文摘要：
This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, "struct" and "union" types, C loops and structured "switch" statements. Clight is the source language of the CompCert verified compiler. The formal semantics of Clight is a big-step operational semantics that observes both terminating and diverging executions and produces traces of input/output events. The formal semantics of Clight is mechanized using the Coq proof assistant. In addition to the semantics of Clight, this article describes its integration in the CompCert verified compiler and several ways by which the semantics was validated.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
