基于BI的带堆操作量子程序推理
量子物理
2024-09-17 v1
摘要
我们为一种带有堆操作、名为Qwhile-hp的量子编程语言提供了良基语义，其中分配语句遵循脏模式，意味着新分配的量子比特可以非确定性地取任意初始状态。为了全面刻画量子环境下的堆操作，我们发展了一种量子BI风格逻辑，包含对分离蕴涵()与分离合取()的解释。随后，我们采用该量子BI风格逻辑作为断言语言来推理带堆操作的量子程序，并提出了一种可靠且相对完备的量子分离逻辑。最后，我们应用该框架验证了多种实用量子程序的正确性，并证明了脏辅助量子比特的正确用法。
引用
@article{arxiv.2409.10153,
title = {BI-based Reasoning about Quantum Programs with Heap Manipulations},
author = {Bonan Su and Li Zhou and Yuan Feng and Mingsheng Ying},
journal= {arXiv preprint arXiv:2409.10153},
year = {2024}
}