Atelier B - Доказательство обязательств формата «H => vv$1 = vv$2» для vv, используемого в замене WHILE.

Question

Я пытаюсь понять Proof Obligations этого формата:H => vv$1 = vv$2vv — это переменная, используемая в реализации в подстановке WHILE. Что означает это ЗП и как это доказать? Спасибо

Вот структура проекта B:

• головка машин, утилиты, главная
• реализации:main_i

Код следующий:

голов.мч

      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

основной.мч

      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