AI 中文总结
该研究从期望运行时分析角度重新审视量子最弱前置条件，引入新的预期望框架，无需上界就能推理其前置条件，给出程序变换等方法，可分析潜在期望运行时无限的量子程序的运行时行为。
AI 中文摘要
量子最弱前置条件是量子程序验证的基本工具，文献中有多种变体。我们从量子程序期望运行时分析的角度重新审视它，引入一个新的预期望框架，无需上界就能推理量子程序的前置条件，这对含奖励语句的量子程序尤为有趣。总体目标是分析潜在期望运行时无限的程序的运行时行为。本文给出了几种实现方法，如一种程序变换，使量子程序的期望运行时能用带奖励的最弱预期望演算来表达。
英文摘要
Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.
