Assignment0320.md

梁亚伦 521030910331 liangyalun@sjtu.edu.cn

1. 不成立. 循环执行结束后 x == 12.

2. 成立. 不能使用 False 作为循环不变量, 因为循环执行前 False 并不成立. 可以使用 True 作为循环不变量.

3. y <= x * 2.

4. s == 1 + 2 + ... + n && 1 + 2 + ... + (n - 1) <= m.

5. x == n && i * i <= n.

6. l <= r && x == n && x < r * r && x >= l * l.

7. exists x'. 100 <= x' + y + z && x' <= 0 && x == 0.

8. exists x'. 0 <= x' + y <= 100 && x' * y <= 100 && x == x' + y.

9. exists y'. exists x'. x' == m && y' == n && x == x' + n && y == x - y'.

10. (1) s * t == 1000 && t == 10; (2) exists s'. s' * t == 1000 && t == 10 && s == s' * t; (3) C.

11. (1) x == n + m && x - y == n. (2) exists y'. x == n + m && x - y' == n && y == x - y'. (3) C. (4) BC. A: 有 ${Q}c{P},{Q}c{R}$; 由最强后条件定义, $P$ 可推出 $R$, 故不成立. B: P = True, e = 0, Q = True, R = x == 0; C: P = x == 0, e = 0, Q = True, R = x == 0.