不变量

在程序语义中，一段代码的不变式（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...
}

不变式在无法在每一步执行详尽检查的复杂系统中尤其有用。我们在系统边界建立不变式，然后任何后续代码都可以假设这些属性成立，而无需再次检查它们。

一般来说，任何可以被假定为真的东西都是不变式。例如，一个规范可以留一个特性为实现定义，但带有某些不变式，这意味着无论具体行为如何，这些属性将始终为真。