Chapter 6: Quantum Hoare logic
Abstract
In this chapter, we define a Hoare-style logic for reasoning about correctness of quantum programs, called quantum Hoare logic. The related notion of weakest precondition is introduced for quantum programs. Using it, the (relative) completeness of quantum Hoare logic is proved.
Keywords
Quantum predicates; Partial correctness; Total correctness; Weakest preconditions; Weakest liberal preconditions; Proof system; Auxiliary rules
A simple quantum programming language, namely quantum while-language, was defined in Chapters 5 to write sequential quantum programs with classical control. It was shown by several examples to be convenient to program some quantum algorithms.
As is well-known, programming is error-prone. ...
Get Foundations of Quantum Programming, 2nd Edition 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.
