迴圈不變式是一種條件式（必須滿足的條件，對迴圈而言是保持不變的，無論迴圈執行了多少次），迴圈語句沒執行一次，就要求中間的結果必須符合不變式的要求。

• （1）進入迴圈語句時，不變式必須成立；
• （2）迴圈語句的迴圈體不能破壞不變式。也就是說，迴圈體開始迴圈時不變式成立，結束時也必須成立；
• （3）如果迴圈語句終止時不變式，依舊成立，那麼至少說明，迴圈在保持迴圈不變式上沒有犯錯。          

  // (**) 不變式在進入迴圈之前必須成立
  while () {
      // 迴圈體開始
      ...
      // 迴圈體結束
      // (**) 不變式在此處也必須成立
  }

  以連結串列反轉為例

• import java.util.Arrays;
  
  public class LinkedListReverse {
  
  	public static void main(String[] args) {
  		// TODO Auto-generated method stub
  		Solution test2=new Solution();
  		ListNode head=test2.createLinkedList(Arrays.asList(1,2,3,4,6,5,7));
  		LinkedListReverse test=new LinkedListReverse();
  		head=test.linkedListReverse(head);
  		ListNode.printLinkedList(head);
  	}
  	public ListNode linkedListReverse(ListNode head){
  		//newhead 代表反轉過的新head loop invariant1
  		ListNode newhead = null;
  		//curhead 代表未反轉的head loop invariant2
  		ListNode curhead=head;
  		while(curhead!=null)
  		{
  			//迴圈體執行前必須滿足loop invariant 即newhead 代表反轉過的新head，curhead 代表未反轉的head 
  			ListNode next=curhead.getNext();
  			curhead.setNext(newhead);
  			newhead=curhead;
  			curhead=next;
  			//迴圈體執行後也必須滿足loop invariant 即newhead 代表反轉過的新head，curhead 代表未反轉的head
  		}
  		//跳出迴圈後也必須滿足loop invariant 即newhead 代表反轉過的新head，curhead 代表未反轉的head
  		return newhead;
  	}
  }