作 者：李卫华
作者机构：武汉大学
出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)
年 卷 期：1983年第1期
页 面：61-74页
主 题：归纳法 引理 CDR 计算方法 转步 算法 递归程序 定义信息
摘 要：每一位程序验证工作者都知道,用现有的任何一种理论方法去验证稍大一点的计算机程序,都存在着不可避免的手工几乎不可完成的推理判断工作。这显然使人们作出这样的决策,即把那些需要创造性的工作由人工来做,而把大量琐絮的推理细节交机器完成,进而借助对机器输出的分析寻求更可行的验证方法。在这方面,美国Boyer—Moore两博士作了十分
