一类单元赋值语句型循环不变式的开发方法研究
The Research on Methods of DeveloPing a Class of LooP Invariants of Single-Variable-Assignnent TyPe

依据现有循环不变式的定义和开发策略，阐述了一类单元赋值语句型循环不变式开发方法，同时使用 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