Page 25 - 《软件学报》2026年第1期

22 软件学报 2026 年第 37 卷第 1 期

应一个 λ.
( ) ( )
( )
,
给定一个上述计数器的格局 α, 用 α(A i ) 表示 α(a i +a i ) α B j 表示 α b j +b i . 若 α 对任何 i ⩽ j ⩽ d 都有 α A j+1 =
1+α B j α A j , 则称其为 i-好的; 若 α 是 (i + 1)-好的, 但是 α(A i+1 ) ⩾ (1+α(B i ))α(A i ), 则称其为 i-坏的; 若 α 是
( ( )) ( )
i-好的或对于某个 j ⩾ i 是 j-坏的, 则称 α 是 i-合法的; 若 α 满足对 i ∈ [d] 0 都有 α(B i ) = λ(i), 则称其为对应 λ 的格局.
若 α 是 0-好的或 0-合法的, 则可以简称为好的或合法的.
Eval(λ), 我们
假设是对应非平凡编码 λ 的好格局, 令 i 0 = index(λ), 为了从 α 得到一个新的好格局 β 对应编码
先考察 β 在 {B i } i∈[d] 0 上应当满足的条件:


 −1,
 i = i 0




β(B i ) = α(B i )+  1+α(B 0 ), i = i 0 −1 (15)




 0, 其他情形
(
公式 (15) 是根据公式 (14) 唯一确定的. β 在 {A i } i∈[d+1] 0 上的行为不是唯一的, 不妨令 β A i 0 ) = α A i 0 ) , 即不对 A i 0
(
的值做修改, 其他值可以通过不变量推导唯一确定:

 ( ( ))
 α(A 0 ) 1+α B i 0 −1

 , i = 0
 ( )
 2+α B i 0 −1 +α(B 0 )






 α(A 1 )


 , 1 ⩽ i ⩽ i 0 −1

β(A i ) =  2+α(B 0 ) (16)




 α(A 1 ),

 i = i 0


 ∏
 i−1
 ( ( ))
 α(A i )−α(A 1 ) 1+α B j , i 0 +1 ⩽ i ⩽ d +1


j=i 0 +1
i 0 的定义, ( ) ( ) = ... = α(A 1 ), 公式 α(A 1 ) 表示. 显然
注意, 根据 α(B 1 ) = ... = α B i 0 −1 = 0, 因此 α A i 0 (16) 中统一用
计算 β 不是一件容易的事, 在正式构造这样的程序前, 我们需要设计一些基本的程序模块.
● 若计数器 a、a 满足 a+a = A, 需实现操作 A −=1, 只需替换为模块“dec( A): do a −=1 or a −=1”.
对应地, 我们也可以定义“inc( A): do a +=1 or a +=1;”. 对多个计数器“ a 1 ,a 2 ,... ”加减 1 也可以简写作 inc( a 1 ,a 2 ,...)
和 dec( a 1 ,a 2 ,...).
● 若计数器 a、a 满足 a+a = A, 有时我们需要将 A 完全转移到计数器 a 上, 这时可以使用模块“reset( A): loop
a +=1, a −=1;”.
● 有时我们需要控制 loop 循环体被执行的最大次数, 可以使用如图 12 所示的程序实现.

inc ( B )
reset ( B ) loop at most B times M ;
loop b -=1, b +=1, M ;
dec ( B )
loop at most B times M loop at most (1 B+ ) times M
图 12 控制循环的最大次数

M 执行不超
若 b+b = B, 则左侧程序可控制 M 执行不超过 B 次, 同时不影响其他计数器; 右侧程序则可控制
( )
过 (1+ B) 次. 因为不变量中有形如 1+ B j 的因子, 这段程序在后续构造中使用频繁.
A i −=1, 仅使用模块 dec( A i+1 = (1+ B i )A i , 我们
● 若修改了某个 A i 的值, 如 A i ) 替换是不够的. 为了维持不变量
至少还需要同时实现 A i+1 −= (1+ B i ). 对于 i ∈ [d +1] 0 , 令 rdec d,i 表示这一程序模块, 我们可以归纳地给出定义:
rdec d,d+1 只需定义为 dec( A d+1 ) 即可; 对于其他 i ∈ [d] 0 , 对应的程序如图 13 所示. 实现 rdec d,i 的过程中调用了
rdec d,i+1 , 最终 rdec d,0 是 O(d) 长的.

dec ( A ) i
loop at most (1 B+ i ) times rdec d , 1i+ ;
图 13 rdec d,j

定义程序 eval d 用于实现变换 Eval, 由上述分析可知, 我们需要根据当前格局 α 的 index(λ) 确定应该进行什么
操作, 为此我们可以构造一族 eval d,i 分别对应 index(λ) = 1,...,d 的情形, 最后令: