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

Question

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

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

является действительным тройной Hoare .

Я не уверен, что кому-либо разрешено ссылаться на переменную (в данном случае 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 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 _ *