Scholarlink

<p>Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with a while loop since its inception in 2006. This paper presents a solution. We prove the relative completeness in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Weakest precondition calculus and relative completeness of satisfaction-based quantum Hoare logic

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年7月28日

查看全文
  • Xin Sun,
  • Xingchi Su,
  • Xiaoning Bian,
  • Huiwen Wu

摘要

Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with a while loop since its inception in 2006. This paper presents a solution. We prove the relative completeness in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus.