基于Tableau的程序综合方法的完全正确性证明

摘要：

基于Tableau方法的程序综合方法以定理证明为基础,将从规格说明得到程序的过程看作是一个定理证明的过程,如果这个证明存在,那么从证明中可抽取出一个满足该程序规格说明的程序.本文证明了通过程序综合方法构造得到的程序是完全正确的程序.

关键词： 程序综合 变换 定理证明 Tableau方法 程序完全正确性 软件自动化

作者: 高晓雷 缪淮扣

作者单位: 上海大学计算机工程与科学学院(上海)

会议类型: 国内会议

会议名称: 2003中国计算机大会

会议地点: 北京

会议语种:中文

页码: 1517-1521

在线出版日期: 2003-11-01（万方平台首次上网日期，不代表论文的发表时间）