基于规范的概率程序切片
摘要：基于规范的概率程序切片方法的研究 基于规范的概率程序切片方法的研究 本文提出了一种基于规范的概率程序切片方法。我们展示了当概率程序伴随着它们的前置条件和后置条件的规范时，我们可以利用这些语义信息来生成严格比基于数据/控制依赖的传统技术所生成的切片更准确且保留规范的切片。 为了实现这个目标，我们的技术基于通过最大预期变换器--Dijkstra最弱前置条件变换器的概率对应物--向后传播后置条件。该技术具有终止敏感性，可以保持概率程序相对于规范的部分正确性和完全正确性。它是模块化的，具有局部推理原理，并经过了形式上的正确性证明。 作为我们技术的基本技术要素，我们设计并证明了用于确立概率程序的部分和完全正确性的可行的验证条件生成器，它们本身具有一定的研究价值，并可在其他地方进行利用。 在实践方面，我们通过几个实例和概率建模领域的一个案例研究展示了我们方法的适用性。我们还描述了一种用于计算我们技术所生成的切片空间中的最小切片的算法。
作者：Marcelo Navarro and Federico Olmedo
论文ID：2205.03707
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-05-10