  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.
