April 2024
Intermediate to advanced
400 pages
21h 1m
English
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.
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. ...