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

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

(2) 将 a、b、e 分别代入定理 11 的 a、b、c, 可得: perloc(a,e).
推论 10 (WRrR 转换). ∀a∈W, ∀b,c,d∈R, c∈R, d∈R, perloc(a,b,c,d)→perloc(a,b,d).
证明: 已知 a∈W, b∈R, c∈R, d∈R, perloc(a,b,c,d), 求证 perloc(a,b,d). 只需证明 perloc(b,d). 可由将 b、c、d 分别
代入定理 10 的 a、b、c 证明.
推论 11 (WwrW 转换). ∀a,b,d∈W, ∀c∈R, perloc(a,b,c,d)→perloc(a,d).
证明: 已知 a∈W, b∈W, c∈R, d∈W, perloc(a,b,c,d), 求证 perloc(a,d).
(1) 将 b、c、d 分别代入定理 13 的 a、b、c, 可得: perloc(b,d).
(2) 将 a、b、d 分别代入定理 14 的 a、b、c, 可得: perloc(a,d).
推论 12 (WWRrR 转换). ∀a,b∈W, ∀c,d,e∈R, perloc(a,b,c,d,e)→perloc(a,b,c,e).
证明: 已知 a∈W, b∈W, c∈R, d∈R, d∈R, perloc(a,b,c,d,e), 求证 perloc(a,b,c,e). 只需求证 perloc(c,e). 可由将 c、d、
e 分别代入定理 10 的 a、b、c 证明.
推论 13 (WwrrW 转换). ∀a,b,e∈W, ∀c,d∈R, perloc(a,b,c,d,e)→perloc(a,e).
证明: 已知 a∈W, b∈W, c∈R, d∈R, e∈W, perloc(a,b,c,d,e), 求证 perloc(a,e).
(1) 将 b、c、d、e 分别代入推论 8 的 a、b、c、d, 可得: perloc(b,e).
(2) 将 a、b、e 分别代入定理 14 的 a、b、c, 可得: perloc(a,e).

4.4 不满足 perloc 传递性的序列模式举例

第 4.3 节证明了 5 种满足 perloc 传递性的序列模式作为模式转换的定理基础. 实际上, 并非所有长度为 3 的
序列模式都具有 perloc 传递性, 这也是引入 DFA 进行证明的原因. 本节使用反例证明了其余 3 种序列模式 (RWR、
WRR 和 WWR) 不满足 perloc 传递性.
命题 1 (RWR 模式). ∃ a,c∈R, ∃b∈W, perloc(a,b,c)→¬perloc(a,c).
证明: 根据表 3, 将目标替换为: 存在同时满足 a∈R, b∈W, c∈R, perloc(a,b,c), ¬poloc(a,c) 的情况.
通过构造反例证明. 根据 poloc 的定义, 只需构造满足 ext(a,c) 的序列即可 (见图 12).

P0 P1
a: R x=1 c: R x=2
rf
poloc
b: R x=2
图 12 证明 RWR 模式不存在传递性的 Litmus 示例

命题 2 (WRR 模式). ∃a∈W, ∃b,c∈R, perloc(a,b,c)→¬perloc(a,c).
证明: 根据表 3, 将目标替换为: 存在同时满足 a∈W, b∈R, c∈R, perloc(a,b,c), ¬(rf(a,c)∨poloc(a,c)).
通过构造反例证明. 根据 poloc 的定义, 只需构造满足 ext(a,c) 的序列即可满足¬poloc(a,c). 根据 rf 定义, 只需
构造 d∈W 并满足 d≠a∧rf(d,c) 即可满足¬rf(a,c). 通过构造 co(a,d) 满足 d≠a.对应的 Litmus 示例见图 13.

P0 P1
rf
a: W x=1 b: R x=1
co fr poloc
rf
d: W x=2 c: R x=2
图 13 证明 WRR 模式不存在传递性的 Litmus 示例

命题 3 (WWR 模式). ∃a,b∈W, ∃c∈R, perloc(a,b,c)→¬perloc(a,c).
证明: 与命题 2 中的反例类似, 区别在于可直接通过构造 d=b 满足 d≠a.对应的 Litmus 示例见图 14.