经机械化证明正确的 C 语言全局变量重命名
编程语言
2016-07-11 v1
摘要
大多数集成开发环境都附带重构工具。然而，它们的重构操作通常被认为不可靠。因此，开发者在应用自动重构后必须测试其代码。在本文中，我们考虑一种重构操作（C 语言中全局变量的重命名），并证明其核心实现保持了被转换程序可能行为集合不变。该正确性证明依赖于 CompCert C 在 Coq 中提供的 C 语言操作语义。
引用
@article{arxiv.1607.02226,
title = {Renaming Global Variables in C Mechanically Proved Correct},
author = {Julien Cohen},
journal= {arXiv preprint arXiv:1607.02226},
year = {2016}
}
备注
In Proceedings VPT 2016, arXiv:1607.01835