一类单元赋值语句型循环不变式的开发方法研究  

The Research on Methods of Developing a Class of Loop Invariants of Single-Variable-Assignment Type

作　　者：杨黄磊 薛锦云[1] 

机构地区：[1]江西师范大学江西省高性能计算技术重点实验室,江西南昌330022

出　　处：《江西师范大学学报（自然科学版）》2014年第4期378-382,共5页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金重大国际合作项目(61020106009);国家自然科学基金(61272075)资助项目

摘　　要：依据现有循环不变式的定义和开发策略,阐述了一类单元赋值语句型循环不变式开发方法,同时使用Dijkstra最弱前置谓词方法确认了循环不变式的正确性.最后通过典型实例来说明该方法的应用.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.

关 键 词：单元赋值语句 循环不变式 开发策略 最弱前置谓词方法 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]