WHILE替换中变量vv对应证明义务H=>vv$1=vv$2的含义及求证咨询

我正在理解B方法中格式为H => vv$1 = vv$2的证明义务（PO），其中vv是WHILE循环替换实现里用到的变量。以下是对应的B项目结构和代码：

项目结构 #

• 机器：head、utils、main
• 实现：main_i

代码实现 #

head.mch #

MACHINE
    head

SETS
    ELEMENTS = {element0,element1,element2}

END

utils.mch #

MACHINE
    utils

SEES
    head
    
OPERATIONS
      xx <-- addElement (el) = 
         PRE
             el : ELEMENTS &
             el /= element0 &
             xx : seq(ELEMENTS)
         THEN
            xx := xx <- el    
         END
 END

main.mch #

MACHINE
    main

SEES
    head
    
VARIABLES
    vv, INIT

INVARIANT
    vv : seq(ELEMENTS) & INIT : BOOL    

INITIALISATION
  vv := [] || INIT := TRUE 

OPERATIONS         
    Op1 (pp) = 
        PRE
             pp : seq(ELEMENTS) &
             size(pp) > 0 &            
             INIT = TRUE &
             !xx.(xx: dom(pp) => pp(xx) /= element0)
         THEN
             INIT := FALSE 
         END

END

main.imp #

IMPLEMENTATION main_i
REFINES main

SEES
    head
    
IMPORTS
    utils
    
CONCRETE_VARIABLES
    vv, INIT

INVARIANT
    vv : seq(ELEMENTS) & INIT : BOOL    

INITIALISATION
  vv := [];
  INIT := TRUE 

OPERATIONS         
    Op1(pp) = 
        ASSERT
             pp : seq(ELEMENTS) &
             size(pp) > 0 &            
             INIT = TRUE &
             !xx.(xx: dom(pp) => pp(xx) /= element0)
         THEN
             VAR ii IN
                    ii := 1;  
                    WHILE 
                        ii <= size(pp) & ii : dom(pp)  
                    DO
                       vv <-- addElement(pp(ii));
                       ii := ii + 1                           
                   INVARIANT
                      ii : NATURAL1 & ii <= size(pp)+1 & vv: seq(ELEMENTS)           
                   VARIANT
                      size(pp)-ii+1                 
                   END
              END;
              INIT := FALSE
         END
END

一、H => vv$1 = vv$2的含义 #

这是B方法中典型的蕴含式证明义务，各部分含义如下：

• H：前提集合，包含所有需要满足的前置条件，具体到这个场景，H涵盖：
  • Op1操作的ASSERT前置条件（与抽象机器main中Op1的PRE一致）
  • WHILE循环的初始化状态（ii = 1）
  • 循环不变式（ii : NATURAL1 & ii <= size(pp)+1 & vv: seq(ELEMENTS)）
  • 循环守卫条件（ii <= size(pp) & ii : dom(pp)）
  • 调用addElement时的前置约束（由前提推导可得）
• vv$1：循环体执行前变量vv的取值
• vv$2：循环体执行后变量vv的取值

该PO的核心要求是：在所有前提条件都成立的情况下，执行一次循环体后，vv的取值必须与执行前完全一致。

二、如何证明这个PO #

结合当前代码分析，这个PO的出现源于抽象机器与具体实现的行为不一致：抽象机器main中的Op1仅修改INIT，不改变vv；但具体实现main_i的Op1通过循环调用addElement修改了vv，因此触发了要求vv保持不变的精化证明义务。

针对这个场景，证明或解决该PO的思路有以下几种：

1. 修正抽象机器（符合具体实现的预期行为） #

如果具体实现中修改vv是设计意图，那么需要同步更新抽象机器main的Op1，使其明确反映vv的变化。例如，在Op1的THEN块中添加对vv的更新逻辑（比如将pp的所有元素追加到vv），这样精化证明的PO会变为验证具体操作与抽象操作的vv修改行为一致，而非要求vv不变。

2. 修正具体实现（符合抽象机器的行为） #

如果抽象机器的行为是正确的（即Op1不应该修改vv），则需要移除具体实现中循环体里的vv <-- addElement(pp(ii));语句。此时循环体仅递增ii，不会修改vv，自然满足vv$1 = vv$2的要求，PO可直接得证。

3. 合法场景下的标准证明步骤（当vv确实需要保持不变时） #

如果循环体设计上不会修改vv，证明步骤如下：

1. 从前提集合H中提取所有关于vv的约束，确认循环执行前vv的状态。
2. 逐一分析循环体的操作，确认没有任何语句对vv进行赋值或修改。
3. 直接推导得出vv$2 = vv$1，从而满足H => vv$1 = vv$2的蕴含关系。

内容的提问来源于stack exchange，提问作者zb1225