Почему экзистенциальное необходимо в сильнейших постусловиях?

Question

Каждая формулировка самого сильного преобразователя предикатов постусловия, который я видел, представляет правило назначения следующим образом:

sp(X:=E, P) = ∃v. (X=E[v/X] ∧ P[v/X])

Мне интересно, почему экзистенциальная (и, следовательно, экзистенциально квантифицированная переменная "v") необходима в приведенном выше правиле? Мне кажется, что самый сильный преобразователь предикатов постусловий почти идентичен символьной оценке, поскольку вы поддерживаете состояние (отображение переменных на значения) и условие пути (предикат, который должен быть истинным в определенной точке программы). Тем не менее, символическая оценка не опирается на экзистенциальный квантификатор.

Итак, я думаю, что я что-то здесь упускаю. Любая помощь приветствуется!

Answer 1

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

Если у вас есть произвольная привязка к переменным, вы не можете ничего сказать о будущих изменениях состояния в программе, прежде чем посмотреть на них во время анализа.

Символическая оценка запоминает каждый выбранный путь [как разделение пространства состояний], поэтому его не нужно указывать в формуле оценки для решения.

Здесь, однако, вы спорите о каждом возможном пути и, следовательно, нуждаетесь в произвольной формуле для описания поведения.

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

Имея, однако, самое слабое либеральное предусловие, вы знаете, с какого возможного пути вы начинаете, и объединяете все пути вместе для проверки свойств вашей системы.