梁亚伦 521030910331 liangyalun@sjtu.edu.cn
1. ABCD
A: 显然具有交换律.
B: 若 x == y 则不可能满足不交并, 矛盾.
C: 同 B.
D: 析取成立.
2. BC
A: 后条件应为 { x == y && store(z, 0) }.
D: *x == u, **x == *u == 0, ***x == *0 is null pointer dereference.
梁亚伦 521030910331 liangyalun@sjtu.edu.cn
1. ABCD
A: 显然具有交换律.
B: 若 x == y 则不可能满足不交并, 矛盾.
C: 同 B.
D: 析取成立.
2. BC
A: 后条件应为 { x == y && store(z, 0) }.
D: *x == u, **x == *u == 0, ***x == *0 is null pointer dereference.