软件学报

作者：赵旭慧，邓玉欣，符鸿飞

单位：赵旭慧，华东师范大学 上海市高可信计算重点实验室, 上海 20006211,邓玉欣，华东师范大学 上海市高可信计算重点实验室, 上海 20006202,符鸿飞，上海交通大学, 上海 20024003

关键词：概率编程;终止性;断言分析;程序验证

基金：国家自然科学基金（62072176，61832015，61802254）

概率程序将概率推理模型与图灵完备的编程语言相结合，统一了对计算和不确定性知识的形式化描述，能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面，它有助于定性和定量地分析仿射概率程序的终止性，可以验证该概率程序是否以概率1终止，估计期望终止时间的上限，并计算步数N，使得N步后给定程序的终止概率呈指数下降；另一方面，它可以估计一个断言成立的概率区间，这有助于分析变量不确定性对概率程序结果的影响.通过实验表明，PROPER对分析各种仿射概率程序是有效的.

来源：2022年第12期

《软件学报》期刊编辑部

查看软件学报杂志2022年第12期