| 一类单元赋值语句型循环不变式的开发方法研究 |
| |
| 引用本文： | 杨黄磊,薛锦云.一类单元赋值语句型循环不变式的开发方法研究[J].江西师范大学学报(自然科学版),2014,0(4):378-382. |
| |
| 作者姓名： | 杨黄磊 薛锦云 |
| |
| 作者单位： | 江西师范大学江西省高性能计算技术重点实验室,江西 南昌,330022 |
| |
| 基金项目： | 国家自然科学基金重大国际合作项目，国家自然科学基金 |
| |
| 摘 要： | 依据现有循环不变式的定义和开发策略，阐述了一类单元赋值语句型循环不变式开发方法，同时使用 Dijkstra 最弱前置谓词方法确认了循环不变式的正确性。最后通过典型实例来说明该方法的应用。
|
| 关 键 词： | 单元赋值语句 循环不变式 开发策略 最弱前置谓词方法 |
The Research on Methods of DeveloPing a Class of LooP Invariants of Single-Variable-Assignnent TyPe |
| |
| YANG Huang-lei,XUE Jin-yun.The Research on Methods of DeveloPing a Class of LooP Invariants of Single-Variable-Assignnent TyPe[J].Journal of Jiangxi Normal University (Natural Sciences Edition),2014,0(4):378-382. |
| |
| Authors: | YANG Huang-lei XUE Jin-yun |
| |
| Institution: | YANG Huang-lei;XUE Jin-yun;Jiangxi Provincial Key Laboratory for High Performance Computing Technology,Jiangxi Normal University; |
| |
| Abstract: | According to definition of loop invariants and strategy for developing loop invatiants proposed,methods of developing a class of loop invariants of single-variable-assignment type and confirmthe correct of loop invariants by using Dijkstra’s weakest pre-condition method hans been elaborated. Finally,some typical examples to illustrate the application of the methods has been listed. |
| |
| Keywords: | single-variable assignment loop invariants strategy for developing the weakest pre-condition method |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《江西师范大学学报(自然科学版)》浏览原始摘要信息 |
| 点击此处可从《江西师范大学学报(自然科学版)》下载免费的PDF全文 |
