Инвариант Hoare Logic Loop

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}

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

• p: i ≥ 0
• b: i> 0
• S: i: = i − 1.

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

Answer 2

Я не уверен, что это ответит на ваш вопрос, но на всякий случай:

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

Answer 3

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