Program verification is the key technology to ensure the correctness of the program.However

due to essential differences of the classical and quantum world

classical program verification techniques and tools cannot be applied directly to the quantum system.Since quantum programming language is a new formal model of quantum system

the verification problem of quantum program is more urgent and necessary.We investigate the program verification for the reachable set and the terminating set of specific nondeterministic quantum program described respectively by bit flip channel

phase flip channel

depolarizing channel

amplitude damping channel and phase damping channel starting from computational basic states in quantum communication systems.Then

we combine pairwise the above five quantum programs into nondeterministic quantum programs

and merge these nondeterministic quantum programs into three nondeterministic quantum programs in terms of the similarities of the reachable set of five quantum programs

and discuss the problem for termination and divergence of these three nondeterministic quantum programs starting from computational basic states.The results shows that these three nondeterministic quantum programs starting from computational basic state 0 are terminated

while starting from computational basic state 1

the termination and the divergence of nondeterministic quantum program consisted by bit flip channel and depolarizing channel relates to the two parameters describing two quantum channels

the termination and the divergence of nondeterministic quantum program consisted by bit flip channel and phase flip channel relates to one parameter describing bit flip channel

and nondeterministic quantum program consisted by amplitude damping channel and phase damping channel is divergence without the two parameters describing quantum channel.And the results provide theoretical and technical support for verification of quantum communication protocol in quantum information security.