IMPLEMENTATION
        TP3WinnieImp
REFINES
        TP3WinnieMachine
IMPORTS
        C_TableParkings.BASIC_ARRAY_VAR ( 0 .. 10 , 0 .. 600 )
INVARIANT
        C_TableParkings.arr_vrb = TableParkings
INITIALISATION
        C_TableParkings.STR_ARRAY ( 0 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 1 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 2 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 3 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 4 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 5 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 6 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 7 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 8 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 9 , 600 ) ;
        C_TableParkings.STR_ARRAY ( 10 , 600 )
OPERATIONS

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

        Ajout_Voiture ( IdParking ) =
                VAR xx IN
                        xx <-- C_TableParkings.VAL_ARRAY ( IdParking ) ;
                        xx := xx - 1 ;
                        C_TableParkings.STR_ARRAY ( IdParking , xx )
                END ;

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

        Retire_Voiture ( IdParking ) =
                VAR xx IN
                        xx <-- C_TableParkings.VAL_ARRAY ( IdParking ) ;
                        xx := xx + 1 ;
                        C_TableParkings.STR_ARRAY ( IdParking , xx )
                END ;

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

        NbLibre <-- Get_NbLibre ( IdParking ) =
                BEGIN
                        NbLibre <-- C_TableParkings.VAL_ARRAY ( IdParking )
                END ;

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

        NbVoitures <-- Get_NbVoitures ( IdParking ) =
                VAR xx IN
                        xx <-- C_TableParkings.VAL_ARRAY ( IdParking ) ;
                        NbVoitures := 600 - xx
                END

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

END