“万物互联”概念的提出,推动着智慧城市与智能家居等各个智能场景下科技的发展,多场景应用无缝体验成为智慧生活的基石。智能设备无法直接观测相关因素,而是通过网络通信等手段感知环境变化和用户需求,在不确定的条件下进行决策。在现实生活中,也普遍存在不确定性问题,这使得我们需要运用先决条件知识和演绎推理并结合不确定性数据进行推断,预估事件发生的可能性。概率是表示不精确和不完备知识的重要工具,概率编程是在不确定条件下进行推断的重要方法,是从研究实验室走向现实世界的重要一步。它将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能有效地处理复杂的关系模型和不确定性问题。本文提出了一种用于分析与验证仿射概率程序的工具——PROPER。首先,在基于经典命令式程序的语义框架下,我们定义了清晰且具有足够表达能力的概率编程语言,支持十余种概率分布,有助于概率推理模型的构建。此外,为了确保概率推理模型具有良好的可靠性、正确性与稳定性,我们从两方面对它进行分析与验证。一方面,PROPER能分别从定性和定量两个方面分析仿射概率程序的终止性。我们将传统的线性秩上鞅推广到多项式秩上鞅,并通过合成多项式秩上鞅的方法来验证。定性分析旨在验证该概率程序是否以概率1终止（几乎肯定终止）,定量分析旨在计算期望终止时间的上界（期望问题）,以及使终止的概率呈指数下降的步数,即集中界限问题。另一方面,PROPER可以推算一个断言成立的概率区间。我们通过静态分析的方法,探索尽可能多的、不同的程序路径,从而分析断言在每条路径终止时正确的概率。当探索到的程序路径覆盖率足够高时,可以视为是对整个程序进行分析。这有助于分析变量不确定性对概率程序结果的影响,在不完备知识处理系统、元推理、风险分析、认知搜索引擎等人工智能领域具有一定的潜在价值。我们通过实验表明PROPER对分析各种仿射概率程序是有效。