Что означает "сильность" в утверждение "Инвариант конструкции должен быть достаточно силен"?

Рейтинг: 1Ответов: 1Опубликовано: 12.09.2014

Читая книгу "Почувствуй класс" Бертрана Мэйера, вижу слова:

Заметьте: в общем случае нужно крайне тщательно проектировать инвариант, чтобы он позволял применить стратегию последовательной аппроксимации.

  • INV должен быть достаточно слабым, чтобы его можно было применить к некоторому начальному подмножеству, обычно содержащему совсем немного элементов из всего множества.
  • Он достаточно силен, чтобы из него следовала цель Post, когда он выполняется на всем множестве.
  • Он достаточно гибкий, чтобы позволять расширять множество, сохраняя его истинность.

Как понимать "сильнее"?

математика логика
Источник: Stack Overflow на русском

Ответы

▲ 5Принят

Ну, давайте рассмотрим на примере.

Вот классический алгоритм подсчёта НОД:

if (m < 0) m = -m;
if (n < 0) n = -n;
while (m != 0 && n != 0)
{
    if (m > n)
        m -= n;
    else
        n -= m;
}
gcd = m + n;

Давайте подумаем, что у нас инвариант шага.

С одной стороны, очевидно, что в силу проверки m и n всегда положительны или 0. Это — инвариант: в начале он выполняется, а на каждом шаге у нас всегда уменьшаемое не меньше вычитаемого, так что после шага цикла инвариант всё ещё выполняется.

Но это — слабый инвариант, потому что из него не получится нужное постусловие: мы-то хотим доказать, что gcd содержит наибольший общий делитель! А из нашего инварианта это не следует.

Поэтому надо искать более сильное условие. Оно будет такое: m и n всегда положительны (или 0), и НОД(m, n) не меняется!

Первая часть условия нами уже доказана (она совпадает с прежним, слабым инвариантом). Вторая тоже легко следует из того, что НОД(m, n) = НОД(m − n, n). Таким образом, мы видим, что если цикл заканчивается, то в gcd будет ненулевое число из m, n, которое равно искомому НОД (т. к. НОД(m, 0) = m, НОД(0, n) = n).

(Стоит ещё добавить, что алгоритм гарантировано заканчивается, так как на каждом шаге наибольшее из m, n уменьшается хотя бы на 1, но в силу инварианта m и n не могут быть отрицательными, поэтому алгоритм не может продолжаться более чем (m + n) итераций. Вот и первое условие инварианта пригодилось!)