Является ли {true} x:= y { x = y } действительной тройкой Хоара?

Question

Я не уверен что

{ true } x := y { x = y }

является действительной тройкой Хоара.

Я не уверен, что один может ссылаться на переменную (в этом случае, y), без явного определения его сначала либо в теле тройной программы, либо в предварительном условии.

{ y=1 } x := y { x = y } //valid

{true} y := 1; x := y { x = y } //valid

Как это?

Answer 1

Я не уверен что

{ true } x := y { x = y }

является действительной тройкой Хоара.

Тройка должна читаться следующим образом:

"Независимо от начального состояния, после выполнения x:=y х равно у."

и это действительно так. Формальный аргумент, почему это так

1. самая слабая предпосылка x := y данное постусловие { x = y } является { y = y }, а также
2. { true } подразумевает { y = y },

Тем не менее, я полностью понимаю, почему вы испытываете беспокойство по поводу этой тройки, и вы беспокоитесь по уважительной причине!

Тройка плохо сформулирована, потому что условия до и после не дают полезной спецификации. Зачем? Потому что (как вы обнаружили) x := 0; y := 0 также удовлетворяет спецификации, так как x = y держит после исполнения.

Очевидно, что x := 0; y := 0 не очень полезная реализация, и причина, по которой она все еще удовлетворяет спецификации, заключается (по мне) в ошибке спецификации.

Как это исправить:

"Правильный" способ выражения спецификации состоит в том, чтобы убедиться, что спецификация является самодостаточной, используя некоторые метапеременные, к которым программа не может получить доступ (x₀ а также y₀ в этом случае):

{ x=x₀ ∧ y=y₀ } x := y { x=y₀ ∧ y=y₀ }

Вот x := 0; y := 0 больше не удовлетворяет почтовому условию.

Answer 2

{ true } x := y { x = y } является действительной тройкой Хоара. Причина в следующем:

x := y является назначением, поэтому замените это в предварительном условии.
Предварительное условие стоит как {y=y}, что подразумевает {true},

Другими словами, {y=y} => {true},

Answer 3

* Если x:=y, то QQED _*