We present a variant of the quantum relational Hoare logic from (Unruh, POPL 2019) that allows us to use "expectations" in pre- and postconditions. That is, when reasoning about pairs of programs, our logic allows us to quantitatively reason about how much certain pre-/postconditions are satisfied that refer to the relationship between the programs inputs/outputs.

翻译：我们从(Unruh, POPL 2019 ) 提出了量子关系Hoare 逻辑的变体,允许我们在先决条件和前提中使用“预期 ” 。 也就是说,在对两个程序进行推理时,我们的逻辑允许我们在数量上解释某些先期/后期条件在多大程度上满足了程序投入/产出之间的关系。