• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊
论文

Analysis of Loop Invariant Development Technology

Expand
  • (1.Key Laboratory for Highperformance Computing Technology,Jiangxi Normal University,Nanchang 330022;
    2.Jiangxi Science and  Technology Normal University,Nanchang 330013;
    3.Key Labortory for Cmoputer Science,Institute of Software,Chinese Academy of Sciences,Bejing 10080,China)

Received date: 2010-03-05

  Revised date: 2010-06-08

  Online published: 2010-09-02

Abstract

Nowadays,highreliability software is a hot issue in software development. The best way to insure the logical structure of algorithms is the formal derivation and proof,and loop invariant is the key to deriving and proving algorithms formally. But the development of loop invariant is always the most difficult,the most creative and the most challenging issue. This paper studies several typical methods of the existing loop invariant development technology,points out  their basic principles,methods,characteristics and effect. This paper analyses several loop invariant development technologies,and points out some problems,to explore the essential characteristics of loop invariant,thus try to give the research guidance for simple and effective methods.

Cite this article

WAN Songsong1,2,XUE Jinyun1,3,XIE Wuping1 . Analysis of Loop Invariant Development Technology[J]. Computer Engineering & Science, 2010 , 32(9) : 84 -88 . DOI: 10.3969/j.issn.1007130X.2010.

Outlines

/