{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:32Z","timestamp":1780994792939,"version":"3.54.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,12,21]],"date-time":"2021-12-21T00:00:00Z","timestamp":1640044800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2018YFA0306701"],"award-info":[{"award-number":["2018YFA0306701"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"crossref","award":["DP180100691"],"award-info":[{"award-number":["DP180100691"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Center for Quantum Computing"},{"DOI":"10.13039\/100018919","name":"Peng Cheng Laboratory","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100018919","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Transactions on Quantum Computing"],"published-print":{"date-parts":[[2021,12,31]]},"abstract":"<jats:p>Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this article, we propose a quantum Hoare logic for a simple while language that involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably, with novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs. Furthermore, to simplify reasoning in real applications, auxiliary proof rules are provided that support standard logical operation in the classical part of assertions and super-operator application in the quantum part. Finally, a series of practical quantum algorithms, in particular the whole algorithm of Shor\u2019s factorisation, are formally verified to show the effectiveness of the logic.<\/jats:p>","DOI":"10.1145\/3456877","type":"journal-article","created":{"date-parts":[[2021,12,21]],"date-time":"2021-12-21T16:43:51Z","timestamp":1640105031000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["Quantum Hoare Logic with Classical Variables"],"prefix":"10.1145","volume":"2","author":[{"given":"Yuan","family":"Feng","sequence":"first","affiliation":[{"name":"University of Technology Sydney, NSW, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia and Chinese Academy of Sciences, China and Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,12,21]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/107803"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_2_4_2","first-page":"117","volume-title":"Proceedings of the European Symposium on Programming","author":"Barthe Gilles","year":"2018","unstructured":"Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2018. An assertion-based program logic for probabilistic programs. In Proceedings of the European Symposium on Programming. Springer, Cham, 117\u2013144."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.68.3121"},{"key":"e_1_3_2_7_2","volume-title":"Proceedings of the International Conference on Computers, Systems and Signal Processing","author":"Bennett Charles H.","year":"1984","unstructured":"Charles H. Bennett and Gilles Brassard. 1984. Quantum cryptography: Public key distribution and coin tossing. In Proceedings of the International Conference on Computers, Systems and Signal Processing."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.69.2881"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1140\/epjd\/e2003-00242-2"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.02.040"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_16"},{"issue":"03","key":"e_1_3_2_14_2","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1142\/S012905410200114X","article-title":"Verifying probabilistic programs using a Hoare like logic","volume":"13","author":"Hartog J. I. Den","year":"2002","unstructured":"J. I. Den Hartog and Erik P. de Vink. 2002. Verifying probabilistic programs using a Hoare like logic. Int. J. Found. Comput. Sci. 13, 03 (2002), 315\u2013340.","journal-title":"Int. J. Found. Comput. Sci."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_16_2","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger Wybe","year":"1976","unstructured":"Edsger Wybe Dijkstra, Edsger Wybe Dijkstra, Edsger Wybe Dijkstra, Etats-Unis Informaticien, and Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Vol. 613924118. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.68.733"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_2_19_2","volume-title":"An Introduction to the Theory of Numbers","author":"Hardy Godfrey Harold","year":"1979","unstructured":"Godfrey Harold Hardy and Edward Maitland Wright. 1979. An Introduction to the Theory of Numbers. Oxford University Press."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-12732-1","article-title":"States, effects, and operations: Fundamental notions of quantum theory","volume":"190","author":"Kraus Karl","year":"1983","unstructured":"Karl Kraus, Arno B\u00f6hm, John D. Dollard, and W. H. Wootters. 1983. States, effects, and operations: Fundamental notions of quantum theory. Lect. Not. Phys. 190 (1983).","journal-title":"Lect. Not. Phys."},{"key":"e_1_3_2_27_2","article-title":"Quantum relational hoare logic with expectations","author":"Li Yangjia","year":"2019","unstructured":"Yangjia Li and Dominique Unruh. 2019. Quantum relational hoare logic with expectations. arXiv:1903.08357. Retrieved from https:\/\/arxiv.org\/abs\/1903.08357.","journal-title":"arXiv:1903.08357"},{"key":"e_1_3_2_28_2","first-page":"187","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Liu Junyi","year":"2019","unstructured":"Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. 2019. Formal verification of quantum algorithms using quantum Hoare logic. In Proceedings of the International Conference on Computer Aided Verification. Springer, 187\u2013207."},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382781"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/1036296"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.5555\/1972505"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_2_34_2","volume-title":"A Procedural Formalism for Quantum Computing","author":"\u00d6mer Bernhard","year":"1998","unstructured":"Bernhard \u00d6mer. 1998. A Procedural Formalism for Quantum Computing. Master\u2019s thesis."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/909003"},{"key":"e_1_3_2_36_2","article-title":"Verification logics for quantum programs","author":"Rand Robert","year":"2019","unstructured":"Robert Rand. 2019. Verification logics for quantum programs. arXiv:1904.04304. Retrieved from https:\/\/arxiv.org\/abs\/1904.04304.","journal-title":"arXiv:1904.04304"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.021"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/359340.359342"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.5555\/648085.747181"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795293172"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.5555\/3470152.3470199"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_45_2","volume-title":"Mathematical Foundations of Quantum Mechanics","author":"Neumann John Von","year":"1955","unstructured":"John Von Neumann. 1955. Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton, NJ."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.5555\/2994450"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0465-3"},{"key":"e_1_3_2_49_2","article-title":"Reasoning about parallel quantum programs","author":"Ying Mingsheng","year":"2018","unstructured":"Mingsheng Ying, Li Zhou, and Yangjia Li. 2018. Reasoning about parallel quantum programs. arXiv:1810.11334. Retrieved from https:\/\/arxiv.org\/abs\/1810.11334.","journal-title":"arXiv:1810.11334"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"}],"container-title":["ACM Transactions on Quantum Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3456877","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3456877","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:26Z","timestamp":1750195886000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3456877"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,21]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,12,31]]}},"alternative-id":["10.1145\/3456877"],"URL":"https:\/\/doi.org\/10.1145\/3456877","relation":{},"ISSN":["2643-6809","2643-6817"],"issn-type":[{"value":"2643-6809","type":"print"},{"value":"2643-6817","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12,21]]},"assertion":[{"value":"2020-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-12-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}