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 the 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, the Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.

翻译：非确定性选择是一种有用的程序构造，它提供了一种描述程序行为的方式，而无需指定可能实现的细节。它支持程序的逐步精化，这一方法在软件开发中已被证明有效。非确定性已被引入量子程序设计，并且非确定性量子程序的终止性已被广泛分析。在本文中，我们超越终止性分析，研究非确定性量子程序的验证问题，其中性质由关联希尔伯特空间上的厄米算子集合给出。我们提出了用于部分正确性和完全正确性的霍尔型逻辑系统，这些系统相对于其对应的语义正确性既是可靠的，也是相对完备的。为了展示这些证明系统的实用性，我们分析了一些量子算法，例如量子纠错方案、多伊奇算法以及非确定性量子游走。最后，实现了一个辅助自动推理非确定性量子程序的证明助手原型。