| Abstract Implementation of Algebraic Specifications in a Temporal Logic Language |
| |
| 作者姓名： | Lin Huimin Gong Chun Xie Hongliang |
| |
| 作者单位： | InstituteofSoftware,AcademiaSinica,Beijing100080 |
| |
| 基金项目： | This project is supported by National Natural Science Foundation of China. |
| |
| 摘 要： | A formal technique for incorporating two specification paradigms is presented,in which an algebraic specification is implemented by a set of abstract procedures specified in pre and post-condition style.The link between the two level specifications is provided via a translation from terms of algebraic specifications into temporal logic formulae representing abstract programs.In terms of translation,a criterion for an abstract implementation satisfying its specification is given,which allows one to check the consistency between the two levels of specifications.The abstract implementations can be refined into executable code by refining each abstract procedure in it.It is proved that the satisfication relation between a specification and its implementations is preserved by such refinement steps.
|
| 关 键 词： | 程序设计 逻辑语言 代数规范 |
Abstract implementation of algebraic specifications in a temporal logic language |
| |
| Lin Huimin,Gong Chun,Xie Hongliang.Abstract Implementation of Algebraic Specifications in a Temporal Logic Language[J].Journal of Computer Science and Technology,1991,6(1):11-20. |
| |
| Authors: | Huimin Lin Chun Gong Hongliang Xie |
| |
| Affiliation: | Institute of Software Academia Sinica; Beijing; Institute of Software; Academia Sinica; |
| |
| Abstract: | A formal technique for incorporating two specification paradigms is presented in which an algebraic specification is implemented by a set of abstract procedures specified in pre- and post-condition style. The link between the two level specifications is provided via a translation from terms of algebraic specifications into temporal logic formulae representing abstract programs. In terms of translation, a criterion for an abstract implementation satisfying its specification is given, which allows one to check the consistency between the two levels of specifications. The abstract implementations can be refined into executable code by refining each abstract procedure in it. It is proved that the satisfication relation between a specification and its implementations is preserved by such refinement steps. |
| |
| Keywords: | |
| 本文献已被 CNKI 维普 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
