摘要
本文介绍了基于微机的归纳法推理系统．用该系统，作者已证明了一批计算机程序的正确性及一些有价值的程序属性，包括算术表达式编译程序的正确性、ＦＯＲＴＲＡＮ编译程序的正确性、ＬＩＳＰ解释程序的正确性等．文中简介了系统的理论基础、数据类型、总体结构，举例说明了系统的推理能力等．
This paper mainly introduces an induction inference system which the authors have recently implemented on the micro computers. Using this system,the authors have already proved the correctness of many computer programs such as the correctness of an arithmetic expression compiler,FORTRAN compiler and LISP interpreter.
出处
《计算机学报》
EI
CSCD
北大核心
1996年第3期230-236,共7页
Chinese Journal of Computers
基金
国家教委跨世纪优秀人才基金
