不變數

在程式語義中，一段程式碼的不變式（invariant）是指在執行該程式碼的過程中始終為真的一個條件。定義不變式有助於對程式碼的正確性和行為進行推理。

例如，在以下程式碼中

let count = 0;
while (hasMessages()) {
  count++;
  processMessage();
}

我們可以證明 count 是一個非負整數，從開頭到結尾都如此。這意味著在程式碼的任何地方，我們都可以將 count 傳遞給一個期望非負整數的函式，並且該函式將正常工作。

不變式可以透過兩種方式建立：透過程式的性質，或者透過顯式的斷言（執行時檢查）。例如，上面的程式碼沒有執行任何檢查，但由於 count 是一個從 0 開始遞增的整數，我們可以保證它的範圍。如果我們從外部源接收輸入，可以使用檢查在邊界處建立不變式。

function processInput(input) {
  if (input < 0 || !Number.isInteger(input)) {
    throw new Error("Input must be a non-negative integer");
  }
  // Process input...
}

不變式在無法在每一步執行詳盡檢查的複雜系統中尤其有用。我們在系統邊界建立不變式，然後任何後續程式碼都可以假設這些屬性成立，而無需再次檢查它們。

一般來說，任何可以被假定為真的東西都是不變式。例如，一個規範可以留一個特性為實現定義，但帶有某些不變式，這意味著無論具體行為如何，這些屬性將始終為真。