In recent years, quantum computing has gained a substantial amount of momentum, and the capabilities of quantum devices are continually expanding and improving. Nevertheless, writing a quantum program from scratch remains tedious and error-prone work, showcasing the clear demand for automated tool support. We present Qet, a fully automated static program analysis tool that yields a precise expected cost analysis of mixed classical-quantum programs. Qet supports programs with advanced features like mid-circuit measurements and classical control flow. The methodology of our prototype implementation is based on a recently proposed quantum expectation transformer framework, generalising Dijkstra's predicate transformer and Hoare logic. The prototype implementation Qet is evaluated on a number of case studies taken from the literature and online references. Qet is able to fully automatically infer precise upper bounds on the expected costs that previously could only be derived by tedious manual calculations.

翻译：近年来，量子计算获得了显著的发展势头，量子设备的能力持续扩展和提升。然而，从零开始编写量子程序仍然是一项繁琐且易错的工作，这充分体现了对自动化工具支持的迫切需求。我们提出了Qet——一款全自动静态程序分析工具，能够对混合经典-量子程序进行精确的预期代价分析。Qet支持具有中间电路测量和经典控制流等高级特性的程序。该原型实现的核心理念基于近期提出的量子期望变换器框架，该框架推广了Dijkstra的谓词变换器和Hoare逻辑。我们基于文献和在线参考资料中的多个案例研究对原型实现Qet进行了评估。Qet能够全自动地推断出预期代价的精确上界，而这些上界此前仅能通过繁琐的手动计算获得。