程序规约在软件工程中具有重要作用,它是对程序性质的形式化描述,可以帮助程序分析工具理解复杂程序的语义。随着程序库在软件开发过程中的广泛使用,为程序库API生成程序规约具有愈发重要的实用价值。本文聚焦于一类以SMT公式作为程序规约的软件工程方法,它们所依赖的SMT规约普遍来自于人工编写或通过符号执行产生:前者需要较高的人工成本,并且易于出错;后者更加实用和可靠,但是在处理程序库API调用时会遇到许多困难。针对提升符号执行工具对程序库API调用的处理能力,本文工作试图为程序库API生成功能级约束,它以SMT公式的形式描述了在API调用前后程序状态的变化情况,可以帮助符号执行工具简化对API调用代码的分析。目前与程序规约生成相关的研究工作可以分为两类,一类是基于程序分析的方法,一类是基于文档分析的方法。这些方法难以被用于生成功能级约束:一方面是因为它们只关注API某些方面的性质,不能完全反映API对程序状态的变换情况;另一方面,许多方法依赖于领域相关的启发式规则,这限制了方法的通用性和可扩展性。在上述工作的基础上,我们对典型程序库的API文档进行调研,发现相关文档具有概括性强、层次结构清晰、功能描述完整、书写方式规范等特点,从文档为API生成功能级约束具有屏蔽代码实现复杂性、便于与领域知识相结合的优势。本文针对基于API文档的功能级约束生成及其在符号执行中的应用进行了系统化研究,研究内容包括:本文提出了一种基于API文档的功能级约束生成方法Doc2SMT。该方法首先使用一组通用的翻译规则将API文档转换成候选OCL表达式。然后,Doc2SMT指导用户人工地构建领域模型,根据领域模型筛选出领域相关的OCL表达式。最后,Doc2SMT将OCL表达式翻译成SMT约束,并借助测试和SMT求解技术验证约束和代码的功能一致性。本文基于所提出的方法,面向提升符号执行工具对API调用的处理能力进行应用研究,提出了将API约束植入到SPF符号执行工具的Ex SPF方法。该方法通过修改SPF对调用指令的执行方式,扩展SPF的路径条件解析模块,实现了以直接向路径约束中添加API约束来代替对API代码的分析,同时通过监听返回指令的执行来收集路径约束。本文为上述方法进行了工具实现与实验评估。实验结果表明,对于JDK容器类程序库的10个常用容器类的259个公有方法,Doc2SMT成功为182个生成了可以通过动态验证的有效约束,其中180个是经过人工确认的与方法功能一致的正确约束,平均每个方法的约束生成时间约为2分钟。Ex SPF为JDK和Apache容器类程序库的16个静态工具方法生成了699个测试,该数量是SPF的17.5倍,平均每个测试的生成时间约为0.55秒。