Hoare тройной с неизвестной переменной в постусловии

Question

Я рассуждаю об упражнении Хоар Логика.

Я должен найти все логические выражения B и все программы S и P, которые удовлетворяют тройную {true} if B then S; if B then P; {a >= 0}, при условии, что оценка B не может изменить хранилище, но исполнение S может изменить его и изменить значение B ,

В частности, я не знаю, что могу сказать о a, потому что он присутствует только в постусловии, и я никогда не нашел такого примера.

Благодарим за помощь!

Answer 1

(мой предыдущий ответ был неправ.)

Вопрос вроде открытого состава, так как существует бесконечное количество выражений (B) и программ (S и P), удовлетворяющих тройная. Кроме того, тройка достаточно сложна, чтобы предотвратить сокращение задачи до простого общего ответа.

В принципе вы можете разбить его следующим образом:

• Для всех состояний, в которых B является ложным, a >= 0 должны иметь (в противном случае тройным в целом не может держать)
• Для государств, в которых B является true, программа S; if B then P должна гарантировать, что a >= 0
• Это справедливо для всех S, B и P таким образом, что ...
  • либо S делает B ложные и a >= 0
  • или S делает B верно, и ...

т.д.