True Postcondition, with true Precondition In my exam preparation I stumbled across the follwoing exercise regarding pre and postconditions:


As far as I understood the question, we need to express some condition for p, such that if that condition holds for p, then we have that {true} p {true}.

The conclusion I got to when trying to think about it intuitevely is that p could simply be a skip statement, but I found myself wondering what a {true} postcondition implies. I know a {true} precondition means that there is no restriction on inputs, what does it mean for postcondition? What would be such a suitable condition to express p?

Thanks!
A true postcondition means there is no restriction on outputs.

Think about it. The condition x &gt; 5 means: it's true (anything goes), as long as x is greater than 5. The only way for that condition to be invalidated is when x isn't greater than 5. The condition true means: x doesn't even need to be greater than 5. There is no way to invalidate that condition at all. Anything goes.

(If you don't mind, I'll leave the rest to you.)