| Program Constructionby Verifying Specification |
| |
| 引用本文： | Lin Hong,Chen Guoliang. Program Constructionby Verifying Specification[J]. 计算机科学技术学报, 1998, 13(6): 597-607. DOI: 10.1007/BF02946503 |
| |
| 作者姓名： | Lin Hong Chen Guoliang |
| |
| 作者单位： | DepartmentofComputerScienceandTechnologyUniversityofScienceandTechnologyofChina,Hefei230027,P,R.China |
| |
| 摘 要： | A program construction method based on Gamma language is proposed.The problem to be solved is specified by first-order predicate logic and a semantic verification program is constructed directly from the specification.Ways for improving efficiency of the program are also studied.The method differs from the one proposed by Manna and Waldinger,where a program 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 programs of Banatre and Le metayes,which consists in decomposing the specification into an invariant and a termination conditon.
|
| 关 键 词： | 程序合成 高级语言 并行性 |
Program construction by verifying specification |
| |
| Hong Lin,Guoliang Chen. Program construction by verifying specification[J]. Journal of Computer Science and Technology, 1998, 13(6): 597-607. DOI: 10.1007/BF02946503 |
| |
| Authors: | Hong Lin Guoliang Chen |
| |
| Affiliation: | (1) Department of Computer Science and Technology, University of Science and Technology of China, 230027 Heifei, P.R. China |
| |
| Abstract: | 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. |
| |
| Keywords: | Program synthesis very high-level language parallelism and concurrency formal specification first-order logic. |
| 本文献已被 CNKI 维普 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载免费的PDF全文 |
