Program Constructionby Verifying Specification  

作　　者：林洪 陈国良 

出　　处：《Journal of Computer Science & Technology》1998年第6期597-607,共11页计算机科学技术学报（英文版）

摘　　要：A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used for deriving Gamma programsof Banatre and Le Metayer, which consists in decomposing the specification into an invariantand a termination condition.A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used for deriving Gamma programsof Banatre and Le Metayer, which consists in decomposing the specification into an invariantand a termination condition.

关 键 词：Program synthesis very high-level language parallelism and concurrency formal specification first-order logic. 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]