Логика Хоара: как строго уменьшающийся вариант цикла сам по себе доказывает завершение?

Question

Обращаясь к правилу while для полной корректности , WP, кажется, говорит мне, что достаточно просто найти вариант цикла, который строго уменьшается, чтобы доказать завершение.Я не могу с этим согласиться, потому что я что-то упускаю или правило неверное.Рассмотрим

int i = 1000;
while(true) i--;

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

Конечно, в правиле должно быть дополнительное предусловиечто-то вроде i <0 → ¬B </em> (где B - это состояние цикла в схеме аксиомы), так что условие цикла в конечном итоге «ловит» вариант цикла и завершается.

Или я что-то пропустил?

Answer 1

Вариант цикла должен быть натуральным числом.Натуральное число не может уменьшаться после нуля.Используя большие слова, вариант цикла представляет собой значение, которое монотонно уменьшается по отношению к обоснованному отношению.В ваших рассуждениях отсутствует обоснованность.

Answer 2

Обычный порядок "<" обоснован натуральными числами, но не целыми числами. Для того чтобы отношение было обоснованным, каждое непустое подмножество его области должно иметь минимальный элемент. Поскольку можно показать, что нет бесконечной нисходящей цепочки относительно обоснованного отношения, отсюда следует, что цикл с вариантом должен завершаться. </p>

Конечно, условие цикла должно быть ложным в случае минимального элемента!

Однако вариант не обязательно должен быть ограничен натуральными числами. Трансфинитные ординалы также хорошо упорядочены.

Answer 3

Как отмечается в статье в Википедии:

[...] условие B должно подразумевать, что t не является минимальным элементом егоrange, в противном случае предпосылка этого правила будет ложной.

В данном случае B равно true, а t равно i.true не подразумевает минимальности i, поэтому предпосылка правила не соблюдается.