THEORY OPOBalanceX IS
  TP3WinnieInterface,9;
  Initialisation,1;
  XAjout_voiture,2;
  XRetire_Voiture,2;
  XNbLibre,2;
  XNbVoitures,2
END
&
THEORY OPOProofList IS
  btrue & XNbVoitures.2,(_of(4) => _of(5));
  btrue & XNbVoitures.1,(_of(3) => _of(2));
  btrue & XNbLibre.2,(_of(4) => _of(5));
  btrue & XNbLibre.1,(_of(3) => _of(2));
  btrue & XRetire_Voiture.2,(_of(4) => _of(5));
  btrue & XRetire_Voiture.1,(_of(3) => _of(2));
  btrue & XAjout_voiture.2,(_of(4) => _of(5));
  btrue & XAjout_voiture.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