We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) determining if a system is separable across a given bipartition, (iii) checking the transversality of a gate with respect to a given stabilizer code, and (iv) computing post-measurement states for computational basis measurements. Further, this logic is extended to accommodate universal quantum computing by deriving Hoare triples for the $T$-gate, multiply-controlled unitaries such as the Toffoli gate, and some gate injection circuits that use associated magic states. A number of interesting results emerge from this logic, including a lower bound on the number of $T$ gates necessary to perform a multiply-controlled $Z$ gate.

翻译：我们证明，基于海森堡表象的 Gottesman (1998) 克利福德电路语义，催生了一种轻量级的类 Hoare 逻辑，可用于高效地表征一类常见的量子程序。我们的应用包括：(i) 验证辅助量子比特是否可以安全丢弃，(ii) 判断一个系统在给定二分划分下是否可分离，(iii) 检查一个门相对于给定稳定子码的横向性，以及 (iv) 计算计算基测量后的量子态。此外，通过推导 $T$ 门、多控制酉门（如 Toffoli 门）以及一些使用相关魔幻态的量子门注入电路的 Hoare 三元组，该逻辑被扩展以支持通用量子计算。从该逻辑中得出了一些有趣的结果，包括执行多控制 $Z$ 门所需 $T$ 门数量的下界。