%0 Journal Article
%T Program construction by verifying specification<br>Program Constructionby Verifying Specification
%A Lin Hong
%A and Chen Guoliang
%A <br>Lin Hong
%A Chen Guoliang
%J 计算机科学技术学报
%D 1998
%I 
%X 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.
%K Program synthesis
%K very high-level language
%K parallelism and concurrency
%K formal specification
%K first-order logic<br>程序合成
%K 高级语言
%K 并行性
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=F57FEF5FAEE544283F43708D560ABF1B&aid=0BD724EC006C854FF1134BCE3E5FE4A6&yid=8CAA3A429E3EA654&vid=FC0714F8D2EB605D&iid=B31275AF3241DB2D&sid=0A8675156EB60B87&eid=D647AF4730396036&journal_id=1000-9000&journal_name=计算机科学技术学报&referenced_num=0&reference_num=14