循环展开：形式定义及其在测试中的应用

测试过程通常旨在实现高覆盖率，但循环严重限制了覆盖目标，因为迭代次数通常不可预测。大多数测试团队通过采用限制为分支覆盖的极端解决方案来解决此问题，这种方法仅考虑循环执行的迭代次数为一次或零次的情形。这种方法会遗漏仅在两次或更多迭代后才会出现的错误。为了实现更有意义的覆盖，测试策略可能展开循环，即使用迭代次数最多为 n 次的执行（其中 n 大于 1），根据可用计算资源进行实用性选择。虽然循环展开是编译器优化技术中标准的一部分，但其在测试中的应用相对较少。部分原因是该概念虽看似直观，但缺乏普遍接受和精确的规范。本文提供了展开的形式定义和一组形式属性。所有这些属性都通过 Isabelle 证明助理机械地被证明是正确的。使用该定义作为概念基础，我们将一种展开策略应用于现有的自动化测试框架，并报告结果：一旦展开循环超过一次，就检测到多少更多的错误？这些结果提供了展开是否应成为测试生成和测试覆盖率测量标准部分的首次评估。