[1]杨黄磊,薛锦云.一类单元赋值语句型循环不变式的开发方法研究[J].江西师范大学学报(自然科学版),2014,(04):378-382.
　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 Science Edition,2014,(04):378-382.
点击复制

一类单元赋值语句型循环不变式的开发方法研究()
分享到：

《江西师范大学学报》（自然科学版）[ISSN:1006-6977/CN:61-1281/TN]

卷:
期数:
2014年04期
页码:
378-382
栏目:
出版日期:
2014-08-31

文章信息/Info

Title:
The Research on Methods of DeveloPing a Class of LooP Invariants of Single-Variable-Assignnent TyPe
作者:
杨黄磊;薛锦云
江西师范大学江西省高性能计算技术重点实验室,江西 南昌,330022
Author(s):
YANG Huang-lei；XUE Jin-yun
关键词:
单元赋值语句; 循环不变式; 开发策略; 最弱前置谓词方法
Keywords:
single-variable assignment; loop invariants; strategy for developing; the weakest pre-condition method
分类号:
TP391
文献标志码:
A
摘要:
依据现有循环不变式的定义和开发策略，阐述了一类单元赋值语句型循环不变式开发方法，同时使用 Dijkstra 最弱前置谓词方法确认了循环不变式的正确性。最后通过典型实例来说明该方法的应用。
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.

参考文献/References:

[1] Furia C A,Meyer B,Velder S.Loop invariants:analysis,classification,andexamples [EB/OL].
[2012-10-16].http://arxiv.org/abs/1211.4470.
[2] Patrick Cousot,Radhia Cousot.Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints [C].New York:ACM press,1997:238-252.
[3] Mine’A.The octagon abstract domain higher-order and symbolic computation [J].High-Order and Symbolic Computation,2006,19(1):31-100.
[4] Patrick Cousot,Nicolas Halbwachs.Automatic discovery of linear restraints among variables of a program [EB/OL].
[2012-10-17].
[5] EnricRodr’1guez-Carbonell,Deepak Kapur.Automatic generation of polynomial invariants of bounded degree using abstract interpretation [J].Sci Comput Program,2007,64(1):54-75.
[6] EnricRodr’1guez-Carbonell,Deepak Kapur.An abstract interpretation approach for automatic generation of polynomial invariants [J].SAS,2004,3148:280-295.
[7] Michael Colón,Sriram Sankaranarayanan,Henny Sipma.Linear invariant generationusing non-linear constraint solving [J].CAV,2003,2725:420-433.
[8] Michael M D,Cockrell J,Griswold W G,et al.Dynamically discovering likely program invariants to support program evolution [J].IEEE Transactions of Software Engineering,2001,27(2):99-123.
[9] Jeff H Perkings,Michael D Ernst.Efficient incremental algorithms for dynamic detection of likely invariants [EB/OL].
[2013-05-16].http:∥homes.cs.washington.edu/～mernst/pubs/invariants-incremental-fse 2004.pdf.
[10] Christoph Csallner,Nikolai Tillman,Yannis Smaragdakis.DySy:dynamicsymbolic execution for invariant inference [EB/OL].
[2013-07-12].http:∥research.microsoft.com/apps/pubs/default.aspx?id=70511.
[11] Nadia Polikarpova,Ilinca Ciupa,Bertrand Meyer.A comparative study of programmer-written and automatically inferred contracts [EB/OL].
[2013-07-19].http:∥se.inf.ethz.ch/people/polikarpova/publications/issta09.pdf.
[12] Yi Wei,Furia C A,Kazmin N,et al.Inferring better contracts [EB/OL].
[2013-08-16].http:∥doi.ieee computersociety.org/10.1145/1985793.1985820.
[13] Thanhvu Nguyen,Deepak Kapur,Westley Weimer,et al.Using dynamic analysis to discover polynomial and array invariants [EB/OL].
[2013-06-17].http:∥en.wikipedia.org/wiki/International_conference_on_Software_Engineering.
[14] Xue Jinyun.New concept of Loop Invariant and its application [EB/OL].
[2013-03-19].http:∥link.springer.com/chapter/10.1007%2F11808107_1.
[15] Xue Jinyun.Two new strategies for developing loop invariants and their applications [J].Journal of Computer Science and Technology,1993,8(2):147-154.
[16] Xue Jinyun.A unified approach for developing efficient algorithmic programs [J].Journal of Computer Science and Technology,1997,12(4):314-329.
[17] Gries D.The science of programming [M].New York:Springer Verlag,1981.

相似文献/References:

[1]化志章.基于遍历序列恢复二叉树的新解法及其证明[J].江西师范大学学报(自然科学版),2013,(03):268.
　HUA Zhi-zhang.A New Solution with Proof for Reconstructing a Binary Tree from Its Traversals[J].Journal of Jiangxi Normal University:Natural Science Edition,2013,(04):268.

备注/Memo

备注/Memo:
国家自然科学基金重大国际合作项目(61020106009)；国家自然科学基金(61272075)
更新日期/Last Update: 1900-01-01