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.

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