| A Structured Temporal Logic Language:XYZ/SE |
| |
| 作者姓名： | Xie Hongliang Gong Jie C.S.Tang |
| |
| 作者单位： | Instituteofsoftware,AcademiaSinica,Beijing100080 |
| |
| 摘 要： | In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is the basis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a general conpositional verification method in the XYZ system concerning the sequential case.
|
| 关 键 词： | 程序设计 XYZ系统 逻辑语言 |
A structured temporal logic language: ZYZ/SE |
| |
| Xie Hongliang,Gong Jie,C.S.Tang.A Structured Temporal Logic Language:XYZ/SE[J].Journal of Computer Science and Technology,1991,6(1):1-10. |
| |
| Authors: | Hongliang Xie Jie Gong C S Tang |
| |
| Affiliation: | Institute of Software Academia Sinica; Beoing; Institute of Software; Academia Sinica; |
| |
| Abstract: | In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system, we propose
a structured temporal logic language called XYZ/SE, based on XYZ/BE which is the basis language of the XYZ system. A set of
proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional
way. Moreover, we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program. So we have developed
a general compositional verification method in the XYZ system concerning the sequential case. |
| |
| Keywords: | |
| 本文献已被 CNKI 维普 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
