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:
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
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:
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
pp
, as it is also the name of a command in the interactive prover.