Floyd--hoare logic for quantum programs | ACM Transactions on Programming Languages and Systems
- ️YingMingsheng
- ️Tue Jan 03 2012
Article No.: 19, Pages 1 - 49
Abstract
Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd--Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.
References
[1]
Akatov, D. 2005. The logic of quantum program verification. M.S. thesis, Oxford University Computing Laboratory.
[2]
Altenkirch, T. and Grattage, J. 2005. A functional quantum programming language. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS'05). 249--258.
[3]
Apt, K. R. and Olderog, E. R. 1997. Verification of Sequential and Concurrent Programs. Springer, Berlin.
[4]
Baltag, A. and Smets, S. 2004. The logic of quantum programs. In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL'04).
[5]
Baltag, A. and Smets, S. 2006. Lqp: The dynamic logic of quantum information. Math. Structures Comput. Sci. 16, 491--525.
[6]
Bettelli, S., Calarco, T., and Serafini, L. 2003. Toward an architecture for quantum programming. Euro. Phys. J. D 25, 181--200.
[7]
Birkhoff, G. and Von Neumann, J. 1936. The logic of quantum mechanics. Ann. Math. 37, 823--843.
[8]
Brunet, O. and Jorrand, P. 2004. Dynamic quantum logic for quantum programs. Int. J. Quantum Inf. 2, 45--54.
[9]
Chadha, R., Mateus, P., and Sernadas, A. 2006. Reasoning about imperative quantum programs. Electron. Notes Theor. Comput. Sci. 158, 19--39.
[10]
D'Hondt, E. and Panangaden, P. 2006. Quantum weakest preconditions. Math. Structures Comput. Sci. 16, 429--451.
[11]
Feng, Y., Duan, R. Y., Ji, Z. F., and Ying, M. S. 2007. Proof rules for the correctness of quantum programs. Theor. Comput. Sci. 386, 151--166.
[12]
Feng, Y., Duan, R. Y., and Ying, M. S. 2011. Bisimulation for quantum processes. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'11). ACM, New York, 523--534.
[13]
Gay, S. J. 2006. Quantum programming languages: survey and bibliography. Math. Structures Comput. Sci. 16, 581--600.
[14]
Gay, S. J. and Nagarajan, R. 2005. Communicating quantum processes. In Proceedings of the 32nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL'05). ACM, New York, 145--157.
[15]
Grover, L. 1996. A fast quantum mechanical algorithm for database searches. In Proceedings of the 28th Annual ACM Symposium on the Theory of Computing. ACM, New York, 212--219.
[16]
Jorrand, P. and Lalire, M. 2005. Toward a quantum process algebra. In Proceedings of the First ACM Conference on Computing Frontiers. ACM, New York, 111--119.
[17]
Knill, E. H. 1996. Conventions for quantum pseudocode. Tech. rep. LAUR-96-2724, Los Alamos National Laboratory.
[18]
Morgan, C. 1995. Proof rules for probabilistic loops. Tech. rep. PRG-TR-25-95, Programming Research Group, Oxford University.
[19]
Nielsen, I. L. and Chuang, M. A. 2000. Quantum Computation and Quantum Information. Cambridge University Press, Cambridge, UK.
[20]
Ömer, B. 2003. Structural quantum programming. Ph.D. dissertation, Technical University of Vienna.
[21]
Sanders, J. W. and Zuliani, P. 2000. Quantum programming. In Mathematics of Program Construction, Lecture Notes in Computer Science, vol. 1837. Springer, Berlin, 88--99.
[22]
Selinger, P. 2004a. A brief survey of quantum programming languages. In Proceedings of the 7th International Symposium on Functional and Logic Programming. Lecture Notes in Computer Science, vol. 2998, Springer, Berlin.
[23]
Selinger, P. 2004b. Towards a quantum programming language. Math. Structures Comput. Sci. 14, 527--586.
[24]
Von Neumann, J. 1938. On infinite direct products. Compos. Math. 6, 1--77.
[25]
Ying, M. S., Duan, R. Y., Feng, Y., and Ji, Z. F. 2010. Predicate Transformer Semantics of Quantum Programs. Cambridge University Press, 311--360.
[26]
Ying, M. S., Feng, Y., Duan, R. Y., and Ji, Z. F. 2009. An algebra of quantum processes. ACM Trans. Comput. Logic 10, 19, 1.
[27]
Zuliani, P. 2004. Nondeterministic quantum programming. In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL'04).
Information & Contributors
Information
Published In
ACM Transactions on Programming Languages and Systems Volume 33, Issue 6
December 2011
145 pages
Copyright © 2012 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 03 January 2012
Accepted: 01 July 2011
Revised: 01 March 2011
Received: 01 September 2010
Published in TOPLAS Volume 33, Issue 6
Permissions
Request permissions for this article.
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- Downloads (Last 12 months)543
- Downloads (Last 6 weeks)66
Reflects downloads up to 03 Mar 2025
Other Metrics
Citations
- Xu YBarthe GZhou L(2025)Automating Equational Proofs in Dirac NotationProceedings of the ACM on Programming Languages10.1145/37048789:POPL(1227-1259)Online publication date: 9-Jan-2025
- Amy MLunderville J(2025)Linear and Non-linear Relational Analyses for Quantum Program OptimizationProceedings of the ACM on Programming Languages10.1145/37048739:POPL(1072-1103)Online publication date: 9-Jan-2025
- Abdulla PChen YChen YHolík LLengál OLin JLo FTsai W(2025)Verifying Quantum Circuits with Level-Synchronized Tree AutomataProceedings of the ACM on Programming Languages10.1145/37048689:POPL(923-953)Online publication date: 9-Jan-2025
- Cousot PWang J(2025)Calculational Design of Hyperlogics by Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/37048529:POPL(446-478)Online publication date: 9-Jan-2025
- Minh Do COgata K(2025)An Executable Operational Semantics of Quantum Programs and Its ApplicationSoftware Fault Prevention, Verification, and Validation10.1007/978-981-96-1621-3_2(15-31)Online publication date: 25-Feb-2025
- Rohe TGrätz SKölle MZielinski SStein JLinnhoff-Popien C(2025)From Problem to Solution: A General Pipeline to Solve Optimisation Problems on Quantum HardwareAdvances in Information and Communication10.1007/978-3-031-84460-7_2(21-41)Online publication date: 7-Mar-2025
- Assolini NDi Pierro AMastroeni I(2025)A Static Analysis of EntanglementVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-82703-7_3(50-71)Online publication date: 23-Jan-2025
- Jiang NCheng XWang JWang Z(2024)基于概率克隆的量子程序断点调试SCIENTIA SINICA Physica, Mechanica & Astronomica10.1360/SSPMA-2024-0404Online publication date: 14-Nov-2024
- Xu MFu JJiang HDeng YLi Z(2024)Termination and Universal Termination Problems for Nondeterministic Quantum ProgramsACM Transactions on Software Engineering and Methodology10.1145/369163233:8(1-41)Online publication date: 2-Sep-2024
- Kang CLee JOh H(2024)Statistical Testing of Quantum Programs via Fixed-Point Amplitude AmplificationProceedings of the ACM on Programming Languages10.1145/36897168:OOPSLA2(140-164)Online publication date: 8-Oct-2024
- Show More Cited By
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.