Page 19 - 《软件学报》2025年第9期

3930 软件学报 2025 年第 36 卷第 9 期

(5.2.8) 由 (5.2.7)、(5.1) 以及 gmo 的非对称性推出矛盾.
(5.3) 证明∄x∈W, rf(x,c)∧rf(x,a). 反证法. 假设∃x∈W, rf(x,c)∧rf(x,a).
(5.3.1) 由 (5.3) 中假设 rf(x,c)、已知条件 rfe(b,c) 以及公理 2 可得: b=x.
(5.3.2) 由 (5.3.1) 以及 rf(x,a) 可得: rf(b,a).
(5.3.3) 由 (5.3.2)、fre(b,a) 以及 fr 定义可得: ∃y∈E, rf(y,a)∧co(y,b).
(5.3.4) 由 (5.3.2)、(5.3.3) 以及公理 2 可得: b=y. 进而得到 co(b,b), 矛盾.
(5.4) 由 (5.2) 和 (5.3) 中的结论可得: ppo2(c,a). 进而通过 ppo 的定义和公理 2 可得: gmo(c,a).
(5.5) 由 (5.1) 和 gmo 的传递性可得: gmo(a,c). 由 gmo 的非对称性, 与 (5.4) 推出矛盾.
定理 5 (RWR 模式). ∀a,c∈R, ∀b∈W, perloc(a,b,c)→¬perloc(c,a).
证明: 根据表 3, 将目标替换为: poloc(a,b)∨fr(a,b), poloc(b,c)∨rf(b,c) 证明¬poloc(c,a).
(1) 反证法. 假设 poloc(c,a) 成立.
下面将已知条件中的析取范式展开为 4 种情况分别证明.
(2) 若 poloc(a,b)∧poloc(b,c), 由 poloc 的传递性可知 poloc(a,c), 又由 (1) 以及引理 5 推出矛盾.
(3) 若 fr(a,b)∧poloc(b,c), 由 (1) 以及 poloc 的传递性可知 poloc(b,a), 又由 fr(a,b) 以及引理 7 推出矛盾.
(4) 若 poloc(a,b)∧rf(b,c), 由 (1) 以及 poloc 的传递性可知 poloc(c,b), 又由 rf(b,c) 以及引理 9 推出矛盾.
(5) 若 fr(a,b)∧rf(b,c), 由 (1) 以及引理 10 推出矛盾.
推论 1 (RRW 模式). ∀a∈R, b∈R, c∈W, perloc(a,b,c)→¬perloc(c,a).
证明: 将 a、b、c 分别带入定理 5 中的 c、a、b 可证.
定理 6 (RWRR 模式). ∀a,c,d∈R, b∈W, perloc(a,b,c,d)→¬perloc(d,a).
证明: 根据表 3, 将目标替换为: 已知 perloc(a,b), perloc(b,c), poloc(c,d), 求证¬poloc(d,a).
(1) 反证法. 假设 poloc(d,a) 成立.
(2) 由 poloc(c,d), poloc(d,a) 以及 poloc 的传递性可得: poloc(c,a).
(3) 由 poloc(c,a), perloc(a,b) 以及推论 1 可得: ¬perloc(b,c). 与条件中的 perloc(b,c) 推出矛盾.
定理 7 (W 模式). 仅包含一个写事件的访存事件序列满足 SCPL.
证明: 同定理 2, 证明是显然的.
推论 2 (WR 模式). ∀a∈W, b∈R, perloc(a,b)→¬perloc(b,a) .
证明: 由定理 4 以及逆否命题的推理定律可证.
引理 11. ∀a,b∈W, perloc(a,b)→co(a,b) .
证明: 根据表 3, 将目标替换为: 已知 a∈W, b∈W, poloc(a,b)∨co(a,b), 求证 co(a,b).
我们将目标替换为: 已知 a∈W, b∈W, poloc(a,b), 求证 co(a,b).
(1) 由 b∈W∧poloc(a,b), ppo1 的定义以及公理 2 可得: gmo(a,b).
(2) 由 (1)、a∈W、b∈W 以及 co 的定义可得: co(a,b).
引理 12. ∀a,b∈W, co(a,b)→¬ perloc(b,a).
证明: 由引理 11 以及 co 的非对称性可证.
定理 8 (WW 模式). ∀a,b∈W, perloc(a,b)→¬perloc(b,a) .
证明: 由表 3 和引理 11, 将目标替换为: 已知 co(a,b), 求证¬co(b,a). 由 co 的非对称性可证.
推论 3 (WRR 模式). ∀a∈W, ∀b,c∈R, perloc(a,b,c)→¬perloc(c,a).
证明: 由定理 5 以及否定引入定律可证.
定理 9 (WWR 模式). ∀a,b∈W, ∀c∈R, perloc(a,b,c)→¬perloc(c,a).
证明: 根据表 3 和引理 11, 将目标替换为: 已知 co(a,b), poloc(b,c)∨rf(b,c), 求证¬(poloc(c,a)∨fr(c,a)).
(1) 反证法. 假设 poloc(c,a)∨fr(c,a) 成立.
将条件分以下 4 种情况证明.