%0 Journal Article
%T 一类单元赋值语句型循环不变式的开发方法研究<br>The Research on Methods of DeveloPing a Class of LooP Invariants of Single-Variable-Assignnent TyPe
%A 杨黄磊
%A 薛锦云
%J -
%D 2014
%X 依据现有循环不变式的定义和开发策略，阐述了一类单元赋值语句型循环不变式开发方法，同时使用 Dijkstra 最弱前置谓词方法确认了循环不变式的正确性。最后通过典型实例来说明该方法的应用。<br>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
%K 单元赋值语句
%K 循环不变式
%K 开发策略
%K 最弱前置谓词方法<br>单元赋值语句 循环不变式 开发策略 最弱前置谓词方法
%K 单元赋值语句 循环不变式 开发策略 最弱前置谓词方法
%K 单元赋值语句 循环不变式 开发策略 最弱前置谓词方法
%K 单元赋值语句 循环不变式 开发策略 最弱前置谓词方法
%U http://lkxb.jxnu.edu.cn//oa/darticle.aspx?type=view&id=20140412