// Testprogram:
class BrukKaninInvariant {
    public static void main ( String []args) {    
         Kaningard mittKaninbur = new Kaningard( );

         Kanin kalle = new Kanin("Kalle");
         Kanin petter = new Kanin("Petter");
         Kanin sprett = new Kanin("Sprett");
         Kanin hopp = new Kanin("Hopp");
         Kanin snurr = new Kanin("Snurr");     

        mittKaninbur.settInn(kalle);
        mittKaninbur.settInn(petter);
        mittKaninbur.settInn(sprett);
        mittKaninbur.settInn(hopp);
        mittKaninbur.settInn(snurr);        

        Kanin ut = mittKaninbur.taUt();
              ut = mittKaninbur.taUt();
              ut = mittKaninbur.taUt();
              ut = mittKaninbur.taUt();
              ut = mittKaninbur.taUt(); 
              ut = mittKaninbur.taUt();
              
        System.out.println("FERDIG KANIN-TEST " );
    }
}

class Kaningard {
    private final int MAXANT = 4;
    private Kanin[] denne = new Kanin[MAXANT];
    private int antall;
    // Invariant: 0 <= antall <= MAXANT;
    Kaningard () {
             // true;
            antall = 0;
            // Invarianten holder;
    }
    public void settInn(Kanin k) {
        // Invarianten holder      
        if(antall < MAXANT) {
            assert antall < MAXANT;
	        denne[antall] = k;
	        antall++;
	    }
	    // Invarianten holder    
    }
    public Kanin taUt( ) {
        // Invarianten holder
        if(antall > 0) {
		   antall--;
		   return denne[antall];  
		}   else return null;
		// Invarianten holder
    }
}

class Kanin{
      private String navn;
      public Kanin(String nv) {
           navn = nv;    
      }
      public String hentNavn()  {
          return navn; 
      }
}