THEORY OPOBalanceX IS
  affichage,5;
  Initialisation,1;
  affichageMenu,2;
  affichageMenuParkings,2
END
&
THEORY OPOProofList IS
  btrue & affichageMenuParkings.2,(_of(4) => _of(5));
  btrue & affichageMenuParkings.1,(_of(3) => _of(2));
  btrue & affichageMenu.2,(_of(4) => _of(5));
  btrue & affichageMenu.1,(_of(3) => _of(2));
  Initialisation.1,(_of(1) => _of(2))
END
&
THEORY OPOFormulas IS
  "`Check that the invariant (btrue) is established by the initialisation - ref 3.3'";
  (btrue);
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  "`Check that the invariant (btrue) is preserved by the operation - ref 3.4'";
  (btrue => btrue)
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END