Доказательство окончания (Proving termination)

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

Для доказательства необходимости окончания алгоритма с циклом определяется целочисленная переменная которая уменьшается при каждой итерации цикла, требования к ней

  • Целочисленная
  • Уменьшается при каждой итерации цикла
  • Не может быть меньше нуля

Если такая переменная есть то она когда нибудь дойдет до нуля, а значит алгоритм завершиться.

Переменная, например, может быть определена как кол-во неотстортированных элементов в массиве.

Ссылки на эту заметку

Эта заметка на GitHub

Обсудить на форуме

Последниее изменение: