一句话：提出量子程序的不正确性逻辑，为静态查错提供可靠完备的逻辑基础。
量子程序开发中的查错十分重要，但已有工作多集中于动态分析，难以给出可靠且完备的静态论证。受经典程序的不正确性逻辑启发，本文提出面向量子程序的不正确性逻辑，作为静态查错的逻辑基础。该逻辑中公式的有效性与量子 Hoare 逻辑形成对偶。作者从可达性视角对有效性的定义给出直观解释，并与若干替代形式进行比较，进而给出可靠且完备的推理规则。文章通过 Grover 搜索、量子隐形传态以及 repeat-until-success 程序等示例展示该逻辑的实用性，并基于逻辑规则实现原型静态分析器，以自动化推理过程。
Bug-catching is important for developing quantum programs. Motivated by the incorrectness logic for classical programs, we propose an incorrectness logic towards a logical foundation for static bug-catching in quantum programming. The validity of formulas in this logic is dual to that of quantum Hoare logics. We justify the formulation of validity by an intuitive explanation from a reachability point of view and a comparison against several alternative formulations. Compared with existing works focusing on dynamic analysis, our logic provides sound and complete arguments. We further demonstrate the usefulness of the logic by reasoning several examples, including Grover's search, quantum teleportation, and a repeat-until-success program. We also automate the reasoning procedure by a prototyped static analyzer built on top of the logic rules.