QbC: Quantum Correctness by Construction
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866918011621867520 |
|---|---|
| author | Peduri, Anurudh Schaefer, Ina Walter, Michael |
| author_facet | Peduri, Anurudh Schaefer, Ina Walter, Michael |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_15641 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | QbC: Quantum Correctness by Construction Peduri, Anurudh Schaefer, Ina Walter, Michael Quantum Physics Logic in Computer Science Programming Languages Software Engineering 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. |
| title | QbC: Quantum Correctness by Construction |
| topic | Quantum Physics Logic in Computer Science Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2307.15641 |