В логике Хоара часто проводится различие между частичной и полной правильностью. Частичная корректность означает, что программа выполняет свою спецификацию или не завершается (бесконечный цикл или рекурсия).
Кто-нибудь знает, для чего была введена эта тонкость по поводу завершения? Мне кажется, что полезна только полная корректность: программа выполняет свою спецификацию и завершается. Кто хочет выполнить возможно бесконечный цикл?
Хотя многие случаи прекращения можно решить с помощью незначительного расширения логики Хоара, а другие можно переписать, чтобы решить эту проблему, это верно не для всех случаев.
Таким образом, в общем случае вам может понадобиться использовать сложную конструкцию доказательства, чтобы доказать полную правильность. Этого должно быть более чем достаточно, чтобы оправдать различие между частичной и полной правильностью.
Взглянем на это с другой стороны: когда доказать завершение намного сложнее, чем доказать частичную правильность, практический инженерный подход должен решить, стоят ли дополнительные усилия.
Тот факт, что мы говорим о частичной правильности, не означает, что частичную правильность одинаково полезно доказывать. Мы говорим о частичной правильности, потому что у нас есть метод ее доказательства (логика Хоара), и мы должны понимать ограничения этого метода.
Логику Хора можно использовать для доказательства того, что алгоритм никогда не завершается с неверным результатом (частичная правильность), но ее нельзя использовать для доказательства того, что алгоритм всегда завершается с правильным результатом (полная правильность). Они не эквивалентны логически, но если бы у нас не было отдельных терминов для них, было бы легко наивно предположить, что они эквивалентны.
Используя стандартную логику Хоара, можно доказать только частичную правильность, а прекращение необходимо доказывать отдельно.
Один из способов представить тройку Хоара — это сегмент кода, аннотированный двумя утверждениями., один перед сегментом и один после него. Утверждение — это логический тест, который либо проходит, либо не проходит, когда утверждение достигнуто. Тройка Хоара утверждает, что если первое утверждение никогда не будет ошибочным, то и второе утверждение никогда не будет ошибочным.
По сути, вы не можете написать утверждение, в котором говорится, что строка кода будет достигнута, потому что какое бы условие вы ни написали, утверждение никогда не будет ошибочным, если оно никогда не будет достигнуто. Обратите внимание, что вы можете assert false сказать, что строка кода не будет достигнута, но assert true никогда не будет ошибкой, независимо от того, достигнута она вообще или нет. Следовательно, хотя доказательство с помощью логики Хоара позволяет сделать вывод, что окончательное утверждение в алгоритме (то есть его постусловие) никогда не нарушается, это не означает, что алгоритм завершается.
