@MISC{SCPINVAR.MIZ,
  AUTHOR = {Chen, Jing-Chao},
  TITLE = {Justifying the Correctness of the {F}ibonacci Sequence and the {E}uclide Algorithm by Loop-Invariant},
  NOTE = {This research is partially supported by the National Natural Science
       Foundation of China Grant No. 69873033.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Computing Directly the Result of ``while$<$0'' Program by Loop-Invariant},
  SECTION3 = {An Example: Summing Directly $n$ Integers by Loop-Invariant},
  SECTION4 = {Computing Directly the Result of ``while$>$0'' Program by Loop-Invariant},
  SECTION5 = {An Example: Computing Directly Fibonacci Sequence by Loop-Invariant},
  SECTION6 = {The Construction of ``while$<>$0'' Loop Program},
  SECTION7 = {The Basic Property of ``while$<>$0'' Program},
  SECTION8 = {Computing Directly the Result of ``while$<>$0'' Program by Loop-Invariant},
  SECTION9 = {An Example: Computing Greatest Common Divisor (Euclide Algorithm)
  by Loop-Invariant},
  DAY = {14},
  MONTH = {June},
  YEAR = {2000},
  ADDRESS1 = {Shanghai Jiaotong University},
  SUMMARY = {If a loop-invariant exists in a loop program, computing
its result by loop-invariant is simpler and easier than
computing its result by the inductive method. For this purpose, the article
describes the premise and the final computation result of
the program such as ``while$<$0'', ``while$>$0'', ``while$<>$0'' 
by loop-invariant.
To test the effectiveness of the computation method given in this
article, by using loop-invariant of the loop programs mentioned above,
we justify the correctness of the following three examples:
   Summing $n$ integers (used for testing ``while$>$0''),
   Fibonacci sequence (used for testing ``while$<$0''),
  Greatest Common Divisor, i.e. Euclide algorithm
   (used for testing ``while$<>$0'').}}

