This paper presents the syntax and operational semantics of quantum while-programs, an extension of classical while programs, using pure states for representing quantum states. Although the syntax presented here is the same as in [19], the operational semantics is different due to the use of pure states instead of density matrices for quantum state representation. The transition relation between configurations of the operational semantics is naturally mapped into a rewriting relation between terms that represent configurations in rewriting logic. This mapping allows us to implement an executable operational semantics of quantum while-programs in Maude, a high-level specification/programming language based on rewriting logic. The executable operational semantics is used as a part of a reachability analysis tool, called QRAT, for quantum programs by utilizing the search command, a built-in reachability analyzer in Maude. Specifically, given a system module for the executable semantics, a source term for an initial configuration, and a target term for a target configuration, the search command is used to automatically check whether the target configuration is reachable from the initial configuration. As a case study, we use QRAT to verify the correctness of Quantum Teleportation to demonstrate the usefulness of our approach.