Алгоритм, который «вроде работает», ещё не обязательно правилен. Чтобы обосновать корректность, используют предусловие, постусловие и инвариант цикла.

Что значит «алгоритм корректен»

Алгоритм корректен, если на любом входе, удовлетворяющем предусловию, он завершается и выдаёт результат, удовлетворяющий постусловию.

  • Предусловие (precondition) — что верно для входа, например список не пуст.
  • Постусловие (postcondition) — что верно для результата, например best — наибольший элемент списка.

Если предусловие нарушено, алгоритм ничего не обещает: ошибка на стороне вызывающего кода.

Инвариант цикла

Инвариант — утверждение, истинное перед каждой итерацией цикла. Проверяют три стадии:

  1. Инициализация — перед первой итерацией инвариант верен.
  2. Сохранение — если он верен в начале итерации, то верен и в конце.
  3. Завершение — когда цикл закончился, инвариант и условие выхода дают постусловие.