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

Question

Я рассуждаю об упражнении Hoare Logic.

Я должен найти все логические выражения 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 правда, и...,

и т.п.