/*@
    public invariant
      capacity >= 1;
	@*/
	/*@
      public invariant
      highscores.length == capacity;
	@*/
	/*@
      public invariant
      highscores != null;
	@*/
	/*@
      public invariant
      (\forall int i; (i >= 0 && i < highscores.length); (highscores[i] == null) ==> (i >= size));
	@*/
	/*@
	  public invariant
	  (\forall Highscore h1, h2; \created(h1) && \created(h2); h1 != h2 ==> h1.highscores != h2.highscores);
	@*/
	/*@
      public invariant
      (min == (-1)) <==> (size == 0);
	@*/
	/*@
      public invariant
      min >= (-1) && min < size;
	@*/
	/*@
      public invariant
      min != (-1) ==> (\forall int i; i >= 0 && i < size;
      		highscores[min].score <= highscores[i].score);
	@*/