演算法正確性（algorithm correctness）

一個演算法之所以正確，是因為它對每一個合法輸入都給出正確答案——不是大多數時候，不是在你剛好測到的案例上，而是永遠。這是一道很高的門檻，而且是刻意的。一座橋若撐得住你試過的卡車、卻在一輛你沒試的車下塌陷，那不叫「大致安全」，而是不安全。同樣地，一個能把你試過的每串清單排好、卻把某一串特定清單弄亂的演算法，根本就不是正確的排序演算法。

精確地說，正確性意味著：對每一個滿足前置條件（對輸入所假設的條件）的輸入，演算法都會停下，而且它的輸出滿足後置條件（定義何謂正確答案、與輸入應有的關係）。這裡綁了兩件事——它必須停，而停下時輸出必須對。真正用來確立這點的標準方法不是測試而是推理，而主力工具是迴圈不變量：一個每次繞迴圈都保持為真的陳述。對插入排序而言，不變量是前綴 A[1..i] 永遠保持已排序。迴圈開始前它成立，因為單一元素的前綴顯然已排序。每一趟把 A[i+1] 插入它該在的位置，於是變長的前綴 A[1..i+1] 仍已排序，不變量撐過了這一步。迴圈結束時，i 已抵達 n，所以已排序的前綴就是整個陣列——這正是我們要的。是這一串推理，而非一堆通過的例子，證明了正確性。

為什麼非要證明而不靠測試？因為多數問題有無窮多個實例，沒有任何有限的測試集能涵蓋全部；測試能揭露臭蟲，卻永遠無法證明它們不存在。正確性還可分成兩種值得命名的風味：部分正確性說「只要它停下，答案就對」，而完全正確性再加上「而且它總會停下」。一個演算法可能部分正確、卻在某些輸入上永遠繞圈，這在實務上毫無用處——所以要有真正的保證，你需要正確答案與終止兩者兼具。