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

Question

Учитывая инвариант цикла, Википедия перечисляет, хороший способ создать самые слабые предварительные условия для цикла (из http://en.wikipedia.org/wiki/Predicate_transformer_semantics):

wp(while E inv I do S, R) = 
    I \wedge
    \forall y. ((E \wedge I) \implies wp(S,I \wedge x < y))[x <- y] \wedge
    \forall y. ((\neg E \wedge I) \implies R)[x <- y]
where y is a tuple of fresh variables.

M [x <- N] заменяет все вхождения x в M на N.

Теперь моя проблема - переменная y. \ Forall y, связывает y в выражении, поэтому "y - это кортеж свежих переменных" для меня не разбирается. Является ли y-координата в \forall такой же, как y в "[x <- y]"? Я просто не могу разобрать вышесказанное.

Изменить: Перефразировано, чтобы избежать запроса ссылки.

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

Answer 1

Синтаксис "x <- y" в указанном вами правиле означает одновременную замену нескольких переменных, которые можно считать именованными x ₁, x₂,… x_n, соответственно, другими переменными y₁, y₂,… y_n которые, как вы указываете, связаны в формуле непосредственно сверху \ a forall.

Способ применения правила на практике - выбрать набор переменных, встречающихся в предикате. R, Количество и название этих переменных оставлено на усмотрение лица, которое применяет правило, но должно быть возможно определить обоснованное отношение < между кортежами выбранной арности так, что \forall y. ((E \wedge I) \implies wp(S,I \wedge x < y))[x <- y] будет доказуемо в конце концов.

Это то, что означает статья в википедии, когда говорится: "Слабейшее условие цикла while обычно параметризуется предикатом I называется петлевой инвариант, а обоснованное отношение к пространственному состоянию обозначается < и называется петлевым вариантом. "Это не просто I который должен быть выбран заранее и должен украшать программу, также есть выбор ряда переменных программы, измененных в теле цикла S и происходит в состоянии Eи существование обоснованного порядка < между кортежами значений этих переменных гарантируют, что условие E ложно в конце концов.

Это гораздо проще понять с помощью реальных систем проверки, в которых можно опробовать вещи. Прочтите это руководство до раздела 2.3 Проверка завершения и посмотрите, имеет ли практическая версия того же объяснения больше смысла для вас.