编码准则和不可判定性
摘要：C/C++编程语言被广泛用于关键系统软件的实现。它们是复杂的语言，具有微妙的特性和特点，甚至可能使经验丰富的程序员感到困惑。因此，通常需要对语言进行子集化，即仅使用"更安全"的子集语言，这在大多数功能安全标准中都有相关规定。编码指南是表达语言子集的首选方式。有些指南仅以编程语言及其实现为基础，可以进行自动检查。然而，由于计算的基本限制，有些指南是不可判定的，即它们基于当前和未来算法无法在所有情况下捕获的程序属性。最成熟和广泛使用的编码标准MISRA明确标记了不可判定或可判定的指南。事实证明，这些信息不是次要的，必须考虑它们以充分理解指南的要求。实际上，不可判定性是影响许多编码标准和相关检查工具用户的普遍困惑的常见来源。在本文中，我们以C/C++程序员理解的方式回顾了可判定性和不可判定性的概念。本文对所有不可判定的MISRA C:2012指南进行了系统研究，讨论了不可判定性的原因及其后果。我们特别关注那些具有可判定逼近的不可判定指南，这些逼近不会过度限制源代码。我们还讨论了一些编码指南，其合规性很难，甚至是不可能证明，超出了可判定性问题的范围。
作者：Roberto Bagnara, Abramo Bagnara, Patricia M. Hill
论文ID：2212.13933
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-12-29