Probabilistic separation logic offers an approach to reasoning about imperative probabilistic programs in which a separating conjunction is used as a mechanism for expressing independence properties. Crucial to the effectiveness of the formalism is the frame rule, which enables modular reasoning about independent probabilistic state. We explore a semantic formulation of probabilistic separation logic, in which the frame rule has the same simple formulation as in separation logic, without further side conditions. This is achieved by building a notion of safety into specifications, using which we establish a crucial property of specifications, called relative tightness, from which the soundness of the frame rule follows.

翻译：概率分离逻辑为推理命令式概率程序提供了一种方法，其中分离合取被用作表达独立性属性的机制。该形式体系有效性的关键在于框架规则，它使得对独立概率状态的模块化推理成为可能。我们探索了概率分离逻辑的一种语义表述，在该表述中，框架规则具有与分离逻辑中相同的简洁形式，无需额外的附加条件。这一目标通过将安全性概念纳入规约来实现，并利用该概念建立了规约的一个关键性质，称为相对紧致性，由此可推导出框架规则的正确性。