We investigate the formal semantics of a simple imperative language that has both classical and quantum constructs. More specifically, we provide an operational semantics, a denotational semantics and two Hoare-style proof systems: an abstract one and a concrete one. The two proof systems are satisfaction-based, as inspired by the program logics of Barthe et al for probabilistic programs. The abstract proof system turns out to be sound and relatively complete, while the concrete one is sound only.

翻译：我们调查了一种具有古典和量子构造的简单必要语言的正式语义。 更具体地说,我们提供了一种实用的语义、一种省略语义和两种Hoare式的验证系统:一种抽象的,一种具体的。 两种验证系统都是基于满意度的,这是由Barthe et al 的程序逻辑所启发的概率程序。 抽象的验证系统是健全和相对完整的,而具体系统则只是健全的。