### 5. Verify that the following program segment is correct with respect to the initial assertion *T* and the final assertion: [ (x \le y \land \text{max} = y) \lor (x > y \land \text{max} = x) ] ```plaintext if x <= y then max := y else max := x ``` --- **Solution:** Initial assertion *T* means this segment will always run and everything is always correct at the beginning of the segment. If ( x < y ) initially, *max* is set equal to *y*, so the left side of the final assertion ∨: ((x \le y \land \text{max} = y)) is true. If ( x = y ) initially, *max* is set equal to *y*, so ((x \le y \land \text{max} = y)) is again true. If ( x > y ), *max* is set equal to *x*, so the right side of the final assertion ∨: ((x > y \land \text{max} = x)) is true. Since ∨ is true whenever one or the other or both sides are true, the final assertion is always true and the program segment is correct. 注意使用 mathtex 显示公式