Proponents of software verification have argued that simpler code is easier to verify: that is, that verification tools issue fewer false positives and require less human intervention when analyzing simpler code. We empirically validate this assumption by comparing the number of warnings produced by four state-of-the-art verification tools on 211 snippets of Java code with 20 metrics of code comprehensibility from human subjects in six prior studies. Our experiments, based on a statistical (meta-)analysis, show that, in aggregate, there is a small correlation (r = 0.23) between understandability and verifiability. The results support the claim that easy-to-verify code is often easier to understand than code that requires more effort to verify. Our work has implications for the users and designers of verification tools and for future attempts to automatically measure code comprehensibility: verification tools may have ancillary benefits to understandability, and measuring understandability may require reasoning about semantic, not just syntactic, code properties.

翻译：软件验证的支持者认为，更简洁的代码更易于验证：即在分析简洁代码时，验证工具产生的误报更少，所需的人工干预也更少。我们通过比较四种主流验证工具在211段Java代码片段上生成的警告数量，与六项先前研究中人类受试者对20项代码可理解性指标的评估结果，对这一假设进行了实证验证。基于统计（元）分析的实验表明，总体而言，可理解性与可验证性之间存在微弱相关性（r=0.23）。研究结果支持以下论断：易于验证的代码通常比需要更多验证努力的代码更易理解。我们的工作对验证工具的用户和设计者，以及未来自动测量代码可理解性的尝试具有启示意义：验证工具可能对可理解性产生附带收益，而测量可理解性可能需要推理代码的语义属性而不仅是句法属性。