# 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 > 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.)

• Well since any input is allowed and so is every output, and we are concerned with partial correctnes (not total), p can be anything right? – Stefan Jan 20 '18 at 15:59