Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

QbC: Quantum Correctness by Construction

Anurudh Peduri, Ina Schaefer, Michael Walter

TL;DR

This work introduces Quantum Correctness by Construction (QbC), a by-construction framework for building quantum programs from formal specifications using pre- and postconditions and a holes mechanism. It extends a quantum while language with holes and defines refinement rules for partial and total correctness, proving soundness and completeness of the system. The authors demonstrate QbC through concrete constructions of a fair quantum coin, quantum teleportation, quantum search (including random sampling and Grover), probability boosting, and the Quantum Fourier Transform, illustrating how specification-driven refinement reveals design choices and alternative implementations. The approach aims to aid quantum algorithm design and software taxonomy, and it envisions future integration with mechanized proof assistants and hybrid verification workflows that combine by-construction and post-hoc methods.

Abstract

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

QbC: Quantum Correctness by Construction

TL;DR

This work introduces Quantum Correctness by Construction (QbC), a by-construction framework for building quantum programs from formal specifications using pre- and postconditions and a holes mechanism. It extends a quantum while language with holes and defines refinement rules for partial and total correctness, proving soundness and completeness of the system. The authors demonstrate QbC through concrete constructions of a fair quantum coin, quantum teleportation, quantum search (including random sampling and Grover), probability boosting, and the Quantum Fourier Transform, illustrating how specification-driven refinement reveals design choices and alternative implementations. The approach aims to aid quantum algorithm design and software taxonomy, and it envisions future integration with mechanized proof assistants and hybrid verification workflows that combine by-construction and post-hoc methods.

Abstract

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.
Paper Structure (58 sections, 12 theorems, 92 equations)

This paper contains 58 sections, 12 theorems, 92 equations.

Table of Contents

  1. Introduction
  2. Our Contributions
  3. Related Work
  4. Correctness-by-Construction for Classical Programs
  5. Probabilistic Verification
  6. Quantum Verification
  7. Recent Developments
  8. Organization of the Paper.
  9. Preliminaries
  10. Notation and Conventions
  11. Quantum Computing
  12. Variables
  13. States
  14. Operations
  15. Quantum While Language
  16. ...and 43 more sections

Key Result

lemma 1

Let $P$ be a projection and $Q$ an arbitrary predicate. Then, $P \Rightarrow Q$ holds if, and only if, $\braket{\psi|Q|\psi} = 1$ for every unit vector $\ket \psi$ such that $P\ket\psi = \ket\psi$.

Theorems & Definitions (23)

  • definition 1: Syntax
  • Remark 1
  • definition 2: Denotational semantics
  • definition 3: Predicates and expectation
  • definition 4: Total correctness
  • definition 5: Partial correctness
  • lemma 1
  • definition 6: Syntax
  • definition 7: Refinement for partial correctness
  • Remark 2: Multiple specifications and formal parameters
  • ...and 13 more