Atelier B - Proving simple PO in the context of a loop

Question

How can I prove the following invariant holds in the context of a WHILE substitution: INIT = FALSE => size(vv)>0? it seems to generate a blocking PO relating to the loop.

Here is the structure of the B project:

head.mch

MACHINE
    head

SETS
    ELEMENTS = {element0,element1,element2}

END

utils.mch

MACHINE
    utils

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

main.mch

MACHINE
    main

SEES
    head
    
VARIABLES
    vv, INIT

INVARIANT
    vv : seq(ELEMENTS) & INIT : BOOL    

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

OPERATIONS         
        Op1 (param) = 
        PRE
             param : seq(ELEMENTS) &
             size(param) > 0 &            
             INIT = NOT_COMPLETE &
             !xx.(xx: dom(param) => param(xx) /= element0)
         THEN
             INIT := COMPLETE || vv ::seq(ELEMENTS)
         END

END

main_i.imp

IMPLEMENTATION main_i
REFINES main

SEES
    head
    
IMPORTS
    utils
    
CONCRETE_VARIABLES
    vv, INIT

INVARIANT
    vv : seq(ELEMENTS) & INIT : BOOL &
    (INIT = FALSE => size(vv)>0)

INITIALISATION
  vv := [];
  INIT := TRUE 

OPERATIONS         
    Op1(param) = 
        BEGIN
             VAR ii IN
                    ii := 1;  
                    WHILE 
                        ii <= size(param) & ii : dom(param)  
                    DO
                       vv <-- addElement(vv, param(ii));
                       ii := ii + 1                           
                   INVARIANT
                      ii : NATURAL1 
                      & ii <= size(param)+1 
                      & vv: seq(ELEMENTS)                    
                   VARIANT
                      size(param)-ii+1                 
                   END
              END;
              INIT := COMPLETE
         END
END

The invariant is proved when there is no loop, for example with

Op1(param) = 
 BEGIN    
      vv := vv <- param(1);
      INIT := COMPLETE
 END

Answer 1

The problem here is that the proof of the desired property relies on the post-condition of the loop, which is built as the conjunction of:

• the loop invariant,
• the negation of the loop guard.

Notice that the only property on vv in this post-condition is that it is in seq(ELEMENTS). So you cannot conclude that it is not empty, and that its size is necessarily greater than zero.

So you must include in the invariant the property on vv that is true whenever the loop guard is evaluated and that will be sufficient to prove your goal.

Here, you could add ii-1 <= size(vv) in the loop invariant.