程序推导的表示

软件自动化是提高软件生产率的关键途径之一,而类比程序设计是软件自动化的一条重要途径,它的主要思想是系统地将求解一个问题的程序转化/修改为求解另一个相似但不等同的问题程序。为达到此目标,现在的共识是充分利用从规格说明到程序的推导,即所谓推导类比方法。当前,程序推导的形式化表示成为该领域研究的焦点。在定理证明领域,证明过程的表示早在1968年 de Bruijn 的工作中得到了充分重视。在他所主持的 AUTOMATH 项目中,数学定理证明过程可用一种带类型λ演算的项