Skip to Main Content
Foundations of Quantum Programming, 2nd Edition
book

Foundations of Quantum Programming, 2nd Edition

by Mingsheng Ying
April 2024
Intermediate to advanced content levelIntermediate to advanced
400 pages
21h 1m
English
Morgan Kaufmann
Content preview from Foundations of Quantum Programming, 2nd Edition

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. ...

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Start your free trial

You might also like

Quantum Computing by Practice: Python Programming in the Cloud with Qiskit and IBM-Q

Quantum Computing by Practice: Python Programming in the Cloud with Qiskit and IBM-Q

Vladimir Silva
The Mathematics of Machine Learning

The Mathematics of Machine Learning

Maria Han Veiga, François Gaston Ged

Publisher Resources

ISBN: 9780443159435