Atelier B - Proof obligations of "H => vv$1 = vv$2" format for vv used in WHILE substitution

Question

I am trying to understand Proof Obligations of this format: H => vv$1 = vv$2 vv is a var used in an implementation within a WHILE substitution. What does this PO mean and how to prove it? Thanks

Here is the structure of the B project:

• machines head, utils, main
• implementations: main_i

The code is the following:

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

Answer 1

vv$1 is the value of state variable vv after the operation Op1 completes, according to the specification/machine. In the specification, this state variable is unchanged.

vv$2 is the value of state variable vv after the operation Op1 completes, according to the implementation. In the implementation, this state variable is updated.

For the implementation to be a correct refinement, vv$1 and vv$2 must always be equal. Yet they are not, and the provided implementation is not a correct refinement. So the proof obligation is not valid.

Some additional pieces of advice:

• In machine utils, operation addElement shall distinguish the value of the sequence before and after :

      after <-- addElement (before, el) = 
         PRE
             el : ELEMENTS &
             el /= element0 &
             before : seq(ELEMENTS)
         THEN
            after := before <- el    
         END

• Avoid identifier pp, as it is also the name of a command in the interactive prover.