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

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

来源：软件学报, 2017, 28(04): 786-803.

DOI：10.13328/j.cnki.jos.005195

• 程序证明
• 一致性
• 抽象程序
• 精化
• 分解

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

• 单位
  计算机软件新技术国家重点实验室; 南京大学