Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification. While automata-based verification scales well when specifications are given directly as automata, prior frameworks incur exponential blow-up when translating high-level set-based assertions into automata, which severely limits practicality. We introduce an extended set-based specification language and a specification-to-automata translation algorithm whose complexity is linear in the number of qubits, enabled by controlled automaton construction and qubit reordering. The resulting compact automata enable fully automatic Hoare-style verification of fixed-qubit quantum programs at previously infeasible scales, while substantially improving expressiveness without compromising efficiency.

翻译：Hoare风格验证为推理量子程序的正确性提供了原理性基础，但现有方法无法实现完全自动验证。当规格说明直接以自动机形式给出时，基于自动机的验证具有良好的可扩展性，但先前框架在将高层基于集合的断言转换为自动机时将导致指数级膨胀，严重限制了实用性。我们提出了一种扩展的基于集合的规格说明语言及一种规格说明到自动机的转换算法，该算法通过受控自动机构造与量子比特重排序实现与量子比特数呈线性关系的复杂度。由此产生的紧凑自动机使固定量子比特数的量子程序能够在先前不可行的规模上实现全自动Hoare风格验证，同时在效率不受损的前提下显著提升了表达能力。