Что такое инварианты?

Инвариант — это утверждение о состоянии программы, которое должно быть истинным в определённых точках выполнения. Идея пришла из формальной верификации: если мы можем описать, что всегда верно, то можем рассуждать о корректности кода без запуска. Инварианты бывают разные: инварианты класса (объект всегда в допустимом состоянии), инварианты цикла (условие истинно перед каждой итерацией), инварианты данных (например, отсортированность массива).

Зачем нужны инварианты

• Помогают доказывать корректность алгоритмов формально.
• Служат документацией: явно описывают, что всегда должно быть верно.
• Позволяют ловить ошибки раньше через assert и проверки в тестах.
• Упрощают рефакторинг: если инвариант сохраняется, поведение не ломается.

Пример: инвариант цикла

Рассмотрим поиск максимума в массиве. Инвариант: после обработки первых i элементов переменная max хранит максимум среди них.

function findMax(arr) {
  let max = -Infinity;
  for (let i = 0; i < arr.length; i++) {
    // Инвариант: max — максимум среди arr[0..i-1]
    if (arr[i] > max) max = arr[i];
    // Инвариант сохранён: max — максимум среди arr[0..i]
  }
  return max;
}

Инварианты класса

В ООП инвариант класса — это условие, которое истинно для любого корректного объекта. Например, у класса «Банковский счёт» баланс не может быть отрицательным.

class Account {
  #balance = 0;
  // Инвариант: balance >= 0
  deposit(amount) {
    if (amount <= 0) throw new Error('Invalid amount');
    this.#balance += amount;
  }
  withdraw(amount) {
    if (amount > this.#balance) throw new Error('Insufficient funds');
    this.#balance -= amount;
  }
}

Как проверять инварианты

1. Использовать assert в критических точках (в dev-сборках).
2. Писать тесты, которые проверяют инвариант после каждой операции.
3. Применять инструменты вроде Design by Contract (например, в Eiffel, Dafny).

Инварианты полезно применять при проектировании алгоритмов, работе с конкурентностью (например, инварианты блокировок) и в критичных системах, где важна корректность. Они делают код понятнее и надёжнее, а также помогают быстрее находить причины багов.