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

Учитывая инвариант цикла, Википедия перечисляет хороший способ создать самые слабые предварительные условия для цикла (из 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]"? Я просто не могу разобрать вышесказанное.

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

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


hoare-logic loop-invariant formal-verification formal-methods formal-semantics
person Jove    schedule 11.10.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Синтаксис «x ‹- y» в правиле, которое вы цитируете, означает одновременную подстановку нескольких переменных, которые можно считать названными x1, x2, … x n соответственно другими переменными y1, y2, … yn, которые, как вы указываете, непосредственно выше в формуле через \forall.

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

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

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

person Pascal Cuoq    schedule 12.10.2014
comment
Большое спасибо за ответ. Я все еще немного смущен; если я заменю y на x в выражении, которое содержит, среди прочего, x ‹ y, то я получу y ‹ y, что никогда не должно быть правдой. - person Jove; 15.10.2014
comment
@Jove wp(…) не является логической функцией. Вы не можете заменить его аргументы. Это метафункция (которая принимает логические термины в качестве аргументов). - person Pascal Cuoq; 15.10.2014
comment
Спасибо. Могу ли я сказать следующее: сначала получите wp(S, I \wedge x ‹ y), назовите это T, а затем подставьте y вместо x в ((E \wedge I) \implies T), так что x и y оба равны связаны \forall y... ? - person Jove; 15.10.2014
comment
@Jove Да, ты можешь так сказать. - person Pascal Cuoq; 15.10.2014
comment
Не могли бы вы, ребята, привести простой пример того, как вам удается делать эти текстовые замены для цикла? Мне нужно решить такое упражнение, и я почти в отчаянии. Заранее спасибо. - person Ilian Vasilev Kulishev; 28.05.2016