Command S is usually designed to establish the truth of a postcondition R. We may not be interested in wp(S,R). If we can find a stronger precondition Q that represents a subset of the set wp(S,R)and can show Q => wp(S,R) then we are content with Q as the postcondition.
Command S is usually designed to establish the truth of a postcondition R. We may not be interested in wp(S,R). If we can find a stronger precondition Q that represents a subset of the set wp(S,R)and can show Q => wp(S,R) then we are content with Q as the postcondition.
When we write {Q} p {R} we denote Total Correctness
Q {p} R denotes partial correctness.