Hoare Logic Loop Invariant

Question

Я смотрю на Hoare Logic, и у меня возникают проблемы с пониманием метода поиска инварианта цикла.

Может кто-нибудь объяснить метод, используемый для вычисления инварианта цикла?

И что должно содержать инвариант цикла, чтобы быть «полезным»?

Я дело только с простыми примерами, находя инварианты и доказательства частичной и полной коррекции в примерах, как:

{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 } 

Answer 1

Если мы говорим о логике Хоары для доказательства (частичная) правильности программ, то вы используете предпосылку и постусловие, разлагаются программа и использовать правила системы вывода логики Хоары для создания и доказать индуктивную формулу.

В вашем примере, вы хотите разложить программу, используя правило

{p} while b do S {p^not(b)} <=> {p^b} S {p} 

В вашем случае

• р: я ≥ 0
• б:> 0
• S: i: = i-1.

Итак, на следующем этапе мы сделаем вывод {i ≥ 0^i > 0} i := i−1 {i ≥ 0}. Это можно сделать еще более обоснованным и доказанным. Надеюсь, это поможет.

Answer 2

Быть полезным (для ваших рассуждений) является основной точкой инварианта. Итак, посмотрите на пост-условие, которое вы хотите доказать, и попытайтесь составить инвариант, который поможет вам приступить к постусловию шаг за шагом и выводится из кода цикла.

Answer 3

Я не уверен, если это будет ответить на ваш вопрос, но только в том случае, это делает:

• А «инвариант цикла» неформально является констатация факта, что остается верным до и после итерации петля. Он по существу определяет ограничение согласованности программы в отношении этого цикла.
• Я не знаю достаточно о Hoare Logic, чтобы рассказать вам, как будет вычисляться инвариант цикла, но я подозреваю, что такая вещь будет зависеть от языка анализируемого кода более, чем от самого формального языка доказательства , У вас есть формальное алгоритмическое описание, с которым вы работаете? Возможно, я смогу продолжить еще немного.
• Полезный инвариант цикла описывал бы что-то конкретное о состоянии приложения. Например, если вы пишете «Сортировка вставки», полезный циклический инвариант для цикла движения основного элемента будет по существу состоять в том, что (под) список содержит один и тот же набор объектов до и после выполнения цикла и, возможно, те элементы, которые были ранее в отсортированном порядке остаются в отсортированном порядке.