一句话：提出非确定性量子程序的部分与完全正确性Hoare逻辑，证明其可靠且相对完备，并实现证明助手原型。
本文研究非确定性量子程序的验证问题。非确定性选择可用于不指定实现细节地描述程序行为，并支持逐步精化；量子编程中已有工作多关注终止性分析，本文则把性质表示为相关Hilbert空间上Hermitian算子集合。作者提出分别针对部分正确性和完全正确性的Hoare型逻辑系统，并证明它们相对于相应语义正确性既是可靠的又是相对完备的。为展示证明系统的实用性，论文分析了量子纠错方案、Deutsch算法以及一个非确定性量子游走等案例。最后，作者实现了一个证明助手原型，以辅助非确定性量子程序的自动化推理。
Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms such as quantum error correction scheme, Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.