Hoare triple with unknown variable in postcondition

Question

I am reasoning about an Hoare Logic's exercise.

I should find all the boolean expressions B and all the programs S and P which satisfy the triple {true} if B then S; if B then P; {a >= 0}, assuming that the evaluation of B cannot modify the store, but the execution of S may modify it and change the value of B.

In particular, I don't know what I can say about a, because it is present just in the postcondition and I have never found an example like this.

Thanks for your help!

Answer 1

(My previous answer was wrong.)

The question is kind of open-ended since there are an infinite number of expressions (B) and programs (S and P) satisfying the triple. Also, the triple is complex enough to prevent reducing the task to a simple general answer.

Basically you could break it down as follows:

• For all states in which B is false, a >= 0 must hold (otherwise the triple as a whole could not hold)
• For the states in which B is true, the program S; if B then P must ensure that a >= 0
• This holds for all S, B and P such that...
  • either S makes B false and a >= 0
  • or, S makes B true, and ...,

etc.