程序规范是软件工程的重要组成部分,缺乏程序规范的软件其质量和可靠性均难以得到保证。现实中的程序规范大多数使用自然语言撰写,但自然语言存在二义性的问题。形式语言可以准确描述程序规范,然而从自然语言中生成形式语言是很困难的。由于程序的每次正确执行过程蕴含程序规范,而程序的执行轨迹（Trace）是程序执行过程的记录,因此可以从程序轨迹中挖掘形式化规范。时序逻辑语言常用来描述程序规范,PPTL具有完全正则的表达能力而且是可判定的。相较于LTL和CTL等时序逻辑语言,PPTL能够更好地表达程序规范。为此,本文针对如何从可执行程序中挖掘PPTL规范开展研究,主要工作如下:1.构建了存储程序模式的PPTL模式库,从已有程序和相关文献中提取和抽象程序的模式,进一步整理归纳得到PPTL模式库,模式库中的模式分为Occurrence和Order两类共37个模式。作为本文程序规范挖掘工作的基础,PPTL模式库相对已有模式库,具有模式丰富和表达能力强的优点,并允许用户自定义编辑添加模式,具有开放性。2.提出了从可执行程序中挖掘得到PPTL规范的方法。首先,借助动态不变量探测工具Daikon和本文所设计开发的Dtrace Filter工具来生成程序的Trace。进而,设计了基于PPTL范式的规范挖掘算法,利用PPTL范式语义对程序执行轨迹进行挖掘,能够保证规范挖掘过程和结果的正确性,避免了直接使用PPTL语义的困难。3.设计开发了PPTL规范挖掘工具PPTLMiner。依照功能划分,PPTLMiner包括Trace生成器、Trace解析器、PPTL公式解析器、PPTL模式公式实例器以及PPTL模式检测器五个模块,并对各个模块的功能及实现细节进行了详细说明。在此基础上,应用读者–写者问题的C程序和生产者–消费者的Java程序对PPTLMiner进行测试,并对测试结果进行分析,测试结果表明PPTLMiner可以挖掘得到程序的正确规范。最后,在哲学家就餐问题模型上验证PPTLMiner的有效性,并进行了PPTLMiner和已有规范挖掘工具的对比实验,结果表明PPTLMiner具有通用性好和表达能力强的优点。