I understand the weakening rule is a combination of two simpler rules: “precondition strengthening” and “postcondition weakening”.
Suppose $P$ is some unknown piece of code such that the following Hoare triple is partially correct. (All variables in the state vector $(x, y, u, v)$ are of integer type.) $$\{x < y\} \; P \; \{u < v\}$$
How can I decide which of the following Hoare triples are partially correct? (Giving a counterexample if they are not)
a) $\{x < y\} \; P \; \{u \le v\} $
b) $\{x \leq y\} \; P \; \{u < v\} $
c) $\{x \leq y - 2\} \; P \; \{u < v\} $
My Attempt:
a) is partially correct as $\{x < y\} \; P \; \{u < v\} \therefore \{x < y\} \; P \; \{u \le v\} $ as $ \{u \le v\}$ is a weakened post condition.
b) is not partially correct counterexample x = y
c) is partially correct as if P $\{x < y\} \; P \; \{u < v\} \therefore \{x \leq y - 2\} \; P \; \{u < v\} $ as $ \{x \leq y - 2\}$ is a strengthed pre condition.