Logic for quantum programs
Abstract
This chapter develops a logical foundation for reasoning about correctness of quantum programs with classical control. We first define quantum predicates as observables that can properly describe properties of quantum systems. The notion of weakest precondition is then generalized to the case of quantum programs. Furthermore, Floyd-Hoare logic for both partial correctness and total correctness of quantum programs is established. The soundness and (relative) completeness of such a logic are proved. An illustrative example is given to show how this logic can be used in verification of quantum programs. Finally, we study non-commutativity – a distinctive feature between observables of classical systems ...
Get Foundations of Quantum Programming now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
