/**
 *  La classe <code>Annuaire</code> définit les services de base nécessaire pour
 *  la gestion d'un annuaire, c'est-&agrave;-dire : création d'un annuaire,
 *  possibilité d'ajouter ou de supprimer des personnes et test de la présence
 *  d'une personne dans l'annuaire.
 *
 * @author     Marc Champesme
 * @version    Créé le lundi 29 mars 2004
 * @version    Modifié le mardi 30 mars 2004
 * @version    Modifié le mardi 6 avril 2004
 */
public class Annuaire {
	/*@
	  @ invariant getCapacite() > 0;
	  @ invariant getNbPersonnes() >= 0
	  		&& getNbPersonnes() <= getCapacite();
	  @ invariant (\forall int i; i >= 0 && i < getNbPersonnes();
	  			getPersonne(i) != null);
	  @*/
	private Personne[] _lesPersonnes;
	private int nbPersonnes;


	/**
	 *  Initialise un Annuaire dont la capacité initiale en nombre de personnes est
	 *  fixée par le paramètre.
	 *
	 * @param  capacite  Capacité initiale de l'annuaire en nombre de personnes
	 */
	/*@
	  @ requires capacite > 0;
	  @ ensures getCapacite() == capacite;
	  @ ensures getNbPersonnes() == 0;
	  @*/
	public Annuaire(int capacite) {
		_lesPersonnes = new Personne[capacite];
	}


	/**
	 *  Renvoie le nombre de personnes présentes dans l'annuaire.
	 *
	 * @return    Le nombre de personnes présentes dans l'annuaire
	 */
	//@ pure
	public int getNbPersonnes() {
		return nbPersonnes;
	}


	/**
	 *  Renvoie la capacité actuelle de l'annuaire en nombre de personnes. Dans
	 *  cette classe, la capacité fait référence &agrave; la taille de la structure
	 *  de données servant &agrave; mémoriser les personnes (par exemple, s'il
	 *  s'agit d'un tableau, la capacité pourrait correspondre au nombre d'éléments
	 *  du tableau).
	 *
	 * @return    La capacité actuelle de l'annuaire en nombre de personnes
	 */
	//@ pure
	public int getCapacite() {
		return _lesPersonnes.length;
	}


	/**
	 *  Ajoute une personne dans l'annuaire, si elle n'y était pas déj&agrave;
	 *  présente
	 *
	 * @param  unePersonne  La personne &agrave; ajouter
	 * @return              <code>true</code> si la personne a effectivement été
	 *      ajoutée (i.e. l'annuaire a été modifié) ; <code>false</code> sinon
	 */
	/*@
	  @ requires unePersonne != null;
	  @ ensures estPresent(unePersonne);
	  @ ensures \result <==> !\old(estPresent(unePersonne));
	  @ ensures \result ==> (getNbPersonnes() == \old(getNbPersonnes()) + 1);
	  @ ensures !\result ==> (getNbPersonnes() == \old(getNbPersonnes()));
	  @ ensures (\forall int i; i >= 0 && i < \old(getNbPersonnes());
	  					getPersonne(i).equals(\old(getPersonne(i))));
	  @ ensures (\result && \old(getNbPersonnes() == getCapacite()))
	  		==> (getCapacite() == \old(getCapacite()) + 10);
	  @*/
	public boolean ajouter(Personne unePersonne) {
		if (estPresent(unePersonne)) {
			return false;
		}

		if (getNbPersonnes() == getCapacite()) {
			Personne[] newTab;

			newTab = new Personne[getCapacite() + 10];
			for (int i = 0; i < getNbPersonnes(); i++) {
				newTab[i] = _lesPersonnes[i];
			}
			_lesPersonnes = newTab;
		}

		_lesPersonnes[nbPersonnes] = unePersonne;
		nbPersonnes = nbPersonnes + 1;

		return true;
	}


	/**
	 *  Retire une personne de l'annuaire, si elle y était déj&agrave; présente
	 *
	 * @param  unePersonne  La personne &agrave; retirer de l'annuaire
	 * @return              <code>true</code> si la personne a effectivement été
	 *      retirée (i.e. l'annuaire a été modifié), <code>false</code> sinon
	 */
	/*@
	  @ requires unePersonne != null;
	  @ ensures !estPresent(unePersonne);
	  @ ensures \result <==> \old(estPresent(unePersonne));
	  @ ensures \result ==> (getNbPersonnes() == \old(getNbPersonnes()) - 1);
	  @ ensures \result ==> (\forall int i; i >= 0 && i < \old(indexDe(unePersonne));
	  					getPersonne(i).equals(\old(getPersonne(i))));
	  @ ensures \result ==> (\forall int i; i >= \old(indexDe(unePersonne)) && i < getNbPersonnes();
	  					getPersonne(i).equals(\old(getPersonne(i+1))));
	  @ ensures !\result ==> (getNbPersonnes() == \old(getNbPersonnes()));
	  @ ensures !\result ==> (\forall int i; i >= 0 && i < getNbPersonnes();
	  					getPersonne(i).equals(\old(getPersonne(i))));
	  @*/
	public boolean retirer(Personne unePersonne) {
		int index;

		index = indexDe(unePersonne);

		if (index == -1) {
			return false;
		}

		for (int i = index; i < (getNbPersonnes() - 1); i++) {
			_lesPersonnes[i] = _lesPersonnes[i + 1];
		}
		nbPersonnes = nbPersonnes - 1;

		return true;
	}


	/**
	 *  Détermine si la personne passée en paramètre est présente dans l'annuaire
	 *
	 * @param  unePersonne  La personne cherchée
	 * @return              <code>true</code> si la personne est présente dans
	 *      l'annuaire, <code>false</code> sinon.
	 */
	/*@
	  @ requires unePersonne != null;
	  @ ensures \result == (\exists int i;i >= 0 && i < getNbPersonnes();
	  					getPersonne(i).equals(unePersonne));
	  @ pure
	  @*/
	public boolean estPresent(Personne unePersonne) {

		return indexDe(unePersonne) != -1;
	}


	/**
	 *  Renvoie l'index dans l'annuaire (i.e. index permettant d'accéder &agrave;
	 *  cette personne &agrave; l'aide de la méthode <code>getPersonne</code>) de
	 *  la personne passée en paramètre. Si la personne est absente de l'annuaire
	 *  la valeur renvoyée est -1.
	 *
	 * @param  unePersonne  La personne dont on souhaite connaître l'index
	 * @return              index de la personne si la personne est présente dans
	 *      l'annuaire ; -1 sinon
	 */
	/*@
	  @ requires unePersonne != null;
	  @ ensures estPresent(unePersonne) <==> (\result >= 0 && \result < getNbPersonnes());
	  @ ensures estPresent(unePersonne) ==> getPersonne(\result).equals(unePersonne);
	  @ ensures !estPresent(unePersonne) <==> (\result == -1);
	  @ pure
	  @*/
	public int indexDe(Personne unePersonne) {
		int index;

		index = -1;
		for (int i = 0; i < getNbPersonnes() && index == -1; i++) {
			if (_lesPersonnes[i].equals(unePersonne)) {
				index = i;
			}
		}

		return index;
	}


	/**
	 *  Renvoie la personne présente dans l'annuaire &agrave; l'index fourni en
	 *  paramêtre.
	 *
	 * @param  index  Index de la personne cherchée
	 * @return        La personne présente dans l'annuaire &agrave; l'index <code>index</code>
	 */
	/*@
	  @ requires index >= 0 && index < getNbPersonnes();
	  @ ensures estPresent(\result);
	  @ ensures indexDe(\result) == index;
	  @ pure
	  @*/
	public Personne getPersonne(int index) {
		return _lesPersonnes[index];
	}


	/**
	 *  Renvoie sous la forme d'un tableau l'ensemble des personnes présentes dans
	 *  l'annuaire.
	 *
	 * @return    Un tableau de <code>Personne</code> dont les éléments sont les
	 *      personnes présentes dans l'annuaire.
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result.length == getNbPersonnes();
	  @ ensures (\forall int i; i >= 0 && i < getNbPersonnes();
	  				\result[i] != null);
	  @ ensures (\forall int i; i >= 0 && i < getNbPersonnes();
	  				\result[i].equals(getPersonne(i)));
	  @ pure
	  @*/
	public Personne[] getTableauPersonnes() {
		Personne[] newTab;

		newTab = new Personne[getNbPersonnes()];
		for (int i = 0; i < getNbPersonnes(); i++) {
			newTab[i] = _lesPersonnes[i];
		}

		return newTab;
	}

}