【摘要】 <正> 一、引言论证递归程序f=E(f)(1)特性的传统方法有结构归纳法(Bustall)和递归归纳法(McCarthy)等.1977年,Backus 在他的Turing 奖讲演中提出了函数式程序设计系统(即FP 系统),并指出可以发展一种程序代数来论证FP 程序(递归的或非递归的).这种代数方法的优点在于程序员可以直接使用程序设计语言本身陈述程序验证过程,并且不需要具有高深的数学知识.尤其重要的是这种代数方法的处理对象可以是一类程序而不是个别的程序,这就有可能导致许多关于更多还原

【Abstract】 In this paper well-expanded solutions are given for a large class of linearfunctional equations.The gcneral terms of the solutions involve only one condit-ion.Therefore,they are more useful for reasoning about programs than Backus’sexpansion solutions.更多还原