一句话：提出与 Hoare 正确性逻辑对偶的“不正确性逻辑”，用于形式化程序错误与缺陷推理。
程序正确性与不正确性如同一枚硬币的两面。即使开发者追求正确性，也常需花费大量时间推理代码为何出错，包括阅读代码时的非形式推理，以及自动化测试和静态分析工具提供的推理。本文提出一种简单的“不正确性逻辑”，用于程序不正确性推理，并在概念上把它刻画为 Hoare 正确性逻辑的另一面。该逻辑面向缺陷发现而非证明所有行为正确，为理解和组织测试与静态分析中的错误推理提供形式化基础。摘要未报告具体实验评估，主要通过概念论述与逻辑对照阐明其与 Hoare 逻辑的对偶关系。
Program correctness and incorrectness are two sides of the same coin. As a programmer, even if you would like to have correctness, you might find yourself spending most of your time reasoning about incorrectness. This includes informal reasoning that people do while looking at or thinking about their code, as well as that supported by automated testing and static analysis tools. This paper describes a simple logic for program incorrectness which is, in a sense, the other side of the coin to Hoare's logic of correctness.