1
$\begingroup$

In my exam preparation I stumbled across the follwoing exercise regarding pre and postconditions: enter image description here

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!

Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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? $\endgroup$
    – Stefan
    Jan 20, 2018 at 15:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.