specification
        
        COIN ::= nickel | dime
        
        --- Vending -----------------------------------------------
        |  ns, ds, value : N
        |--------------------------------
        |  value = (ns * 5) + (ds * 10);
        |  value <= 100
        -----------------------------------------------------------
        
        --- Insert_Nickel -----------------------------------------
        |  Delta Vending;
        |  coin? : COIN
        |--------------------------------
        |  coin? = nickel;
        |  ns' = ns + 1
        -----------------------------------------------------------
        
        end specification