梁亚伦 521030910331 liangyalun@sjtu.edu.cn
1. 错误.
2. 错误: 首先, c 不一定会终止; 其次, 即使 c 终止, 也不一定会对 x 做任何判断, 例如 c 可以是 (无条件地) y = 0.
3. 正确.
4. 正确. (仅限 SimpleWhile 语言; 在可能出错的语言里 c 还可能出错.)
5. 正确.
6. 正确.
由于 SimpleWhile 语言的执行是确定性的, 且不执行出错, 故我们可以把指称语义简化为一个 sem : (c : statement) -> (s1 : state) -> result 的函数, 其中 result = inf | nrm (s : state).
现在我们来考虑 sem(c_1) 和 sem(c_2) 的值.
- 我们可以把一个 state 表示为一个霍尔三元组的条件. 如果
sem(c_1, s) = inf, 则有${s}c_1{\mathrm{False}}$ , 故有${s}c_2{\mathrm{False}}$ , 故sem(c_2) = inf. - 如果
sem(c_1, s_1) = nrm s_2, 则有${s_1}c_1{s_2}$ , 且${s_1}c_1{\mathrm{False}}$ 不成立; 故有${s_1}c_2{s_2}$ , 且${s_1}c_2{\mathrm{False}}$ 不成立, 即$c_2$ 不会运行不终止,sem(c_2) != inf. 由于$s_2$ 这一条件完整地描述了程序运行后的状态, 故只能sem(c_2) = nrm s_2.
综上, 无论对何 s_1 都有 sem(c_1) = sem(c_2), 即