IMPLEMENTATION
        TP3WinnieImp
REFINES
        TP3WinnieMachine
CONCRETE_VARIABLES
        C_NbPlaces
INVARIANT
        C_NbPlaces : 0 .. 600 &
        C_NbPlaces = NbPlaces
INITIALISATION
        C_NbPlaces := 600
OPERATIONS

        /*------------------------------------------------------*/

        Ajout_Voiture =
                BEGIN
                        C_NbPlaces := C_NbPlaces - 1
                END ;

        /*------------------------------------------------------*/

        Retire_Voiture =
                BEGIN
                        C_NbPlaces := C_NbPlaces + 1
                END ;

        /*------------------------------------------------------*/

        NbLibre <-- Get_NbLibre =
                BEGIN
                        NbLibre := C_NbPlaces
                END ;

        /*------------------------------------------------------*/

        NbVoitures <-- Get_NbVoitures =
                BEGIN
                        NbVoitures := 600 - C_NbPlaces
                END

        /*------------------------------------------------------*/

END