通过抽象程序证明复杂具体程序

来源：软件学报杂志2017年第4期北京时间：

作者：李彬,汤震浩,翟娟,赵建华

单位：李彬，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002311,汤震浩，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,翟娟，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303,赵建华，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002304

摘要：描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构（ADTs），如set，list，map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系、抽象程序程序点和具体程序程序点的对应关系.基于对应关系，抽象程序和具体程序一致性证明可以分解，从而容易并可能自动证明.

关键词：程序证明;一致性;抽象程序;精化;分解

基金资助：国家自然科学基金（61632015，61561146394）；国家重点基础研究发展计划（973）（2016YFB1000802）