/**
 *  La classe CpteBancaireReleve décrit les services de base nécessaire pour la
 *  gestion d'un compte bancaire : c'est-à-dire ouverture d'un compte
 *  avec un solde initial strictement positif, possibilité d'effectuer des
 *  opérations de crédit (i.e. versements) ou de débit (i.e. retraits) et de
 *  consulter le solde (i.e. montant disponible après imputation de chaque
 *  opération de débit ou crédit). <p>
 *
 *  La classe CpteBancaireReleve permet, en plus des opérations précédentes, de
 *  consulter les dernières opérations effectuées et peut donc être utilisée
 *  pour produire un relevé de compte indiquant les dernières opérations
 *  effectuées sur le compte. Le nombre d'opérations mémorisées par défaut est
 *  10, mais peut-être défini librement &agrave; la création de l'instance.
 *  Après la création de l'instance, le nombre d'opérations peut être augmenté,
 *  mais pas diminué.</p>
 *
 * @author     Marc Champesme
 * @version    31 mars 2004
 */
public class CpteBancaireReleve {
	/*@
	  @ invariant getNbOperations() >= 0 && getNbOperations() <= getNbMaxOperations();
	  @ invariant getNbMaxOperations() > 0;
	  @*/


	/**
	 *  Initialise une instance de la classe CpteBancaireReleve en prenant comme
	 *  solde initial la valeur transmise en paramètre et la valeur par défaut pour
	 *  le nombre d'opérations mémorisées. Cette valeur par défaut est fixée
	 *  &agrave; 10. La valeur du solde initial doit être strictement positive.
	 *
	 * @param  soldeInitial  Solde initial du compte
	 */
	/*@
	  @ requires soldeInitial > 0;
	  @ ensures getSolde() == soldeInitial;
	  @ ensures getSoldeAnterieur() == soldeInitial;
	  @ ensures getNbOperations() == 0;
	  @ ensures getNbMaxOperations() == 10;
	  @*/
	public CpteBancaireReleve(double soldeInitial) {
	}


	/**
	 *  Initialise une instance de la classe CpteBancaireReleve en prenant comme
	 *  solde initial la valeur transmise en paramètre et la valeur transmise en
	 *  paramètre pour le nombre d'opérations mémorisées. Les valeurs du solde
	 *  initial et du nombre d'opérations mémorisées doivent être strictement
	 *  positives.
	 *
	 * @param  soldeInitial     Solde initial du compte
	 * @param  nbMaxOperations  Nombre d'opérations mémorisées
	 */
	/*@
	  @ requires soldeInitial > 0;
	  @ requires nbMaxOperations > 0;
	  @ ensures getSolde() == soldeInitial;
	  @ ensures getSoldeAnterieur() == soldeInitial;
	  @ ensures getNbOperations() == 0;
	  @ ensures getNbMaxOperations() == nbMaxOperations;
	  @*/
	public CpteBancaireReleve(double soldeInitial, int nbMaxOperations) {
	}


	/**
	 *  Renvoie la valeur courante du solde du compte.
	 *
	 * @return    La valeur courante du solde du compte
	 */
	/*@
	  @ ensures \result == (\sum int i;
	  				i >= 0 && i < getNbOperations();
	  				getDerniereOperation(i))
			       + getSoldeAnterieur();
	  @
	  @ pure
	  @*/
	public double getSolde() {
	}


	/**
	 *  Renvoie le solde du compte avant imputation des opérations mémorisées..
	 *
	 * @return    La valeur antérieure du solde du compte
	 */
	//@ pure
	public double getSoldeAnterieur() {
	}


	/**
	 *  Enregistre une opération de crédit sur le compte dont le montant est passé
	 *  en paramètre. Le montant du crédit passé en paramètre doit être strictement
	 *  positif.
	 *
	 * @param  credit  Montant de l'opération de crédit
	 */
	/*@
	  @ requires credit > 0;
	  @ ensures getDerniereOperation(getNbOperations() - 1) == credit;
	  @ ensures getSolde() == \old(getSolde()) + credit;
	  @ ensures \old(getNbOperations()) < getNbMaxOperations()
	  		==> getNbOperations() == \old(getNbOperations()) + 1;
	  @ ensures \old(getNbOperations()) < getNbMaxOperations()
	  		==> (\forall int i; i >= 0 && i < \old(getNbOperations());
				getDerniereOperation(i) == \old(getDerniereOperation(i)));
	  @ ensures \old(getNbOperations()) < getNbMaxOperations()
	  		==> getSoldeAnterieur() == \old(getSoldeAnterieur());
	  @ ensures \old(getNbOperations()) == getNbMaxOperations()
	  		==> getNbOperations() == \old(getNbOperations());
	  @ ensures \old(getNbOperations()) == getNbMaxOperations()
	  		==> (\forall int i; i >= 0 && i < (getNbMaxOperations() - 1);
				getDerniereOperation(i) == \old(getDerniereOperation(i + 1)));
	  @ ensures \old(getNbOperations()) == getNbMaxOperations()
	  		==> getSoldeAnterieur() == \old(getSoldeAnterieur() + getDerniereOperation(0));
	  @*/
	public void crediter(double credit) {
	}


	/**
	 *  Enregistre une opération de débit sur le compte dont le montant est passé
	 *  en paramètre. Le montant du débit passé en paramètre doit être strictement
	 *  positif.
	 *
	 * @param  debit  Montant de l'opération de débit
	 */
	/*@
	  @ requires debit > 0;
	  @ ensures getDerniereOperation(getNbOperations() - 1) == - debit;
	  @ ensures getSolde() == \old(getSolde()) - debit;
	  @ ensures \old(getNbOperations()) < getNbMaxOperations()
	  		==> getNbOperations() == \old(getNbOperations()) + 1;
	  @ ensures \old(getNbOperations()) < getNbMaxOperations()
	  		==> (\forall int i; i >= 0 && i < \old(getNbOperations());
				getDerniereOperation(i) == \old(getDerniereOperation(i)));
	  @ ensures \old(getNbOperations()) < getNbMaxOperations()
	  		==> getSoldeAnterieur() == \old(getSoldeAnterieur());
	  @ ensures \old(getNbOperations()) == getNbMaxOperations()
	  		==> getNbOperations() == \old(getNbOperations());
	  @ ensures \old(getNbOperations()) == getNbMaxOperations()
	  		==> (\forall int i; i >= 0 && i < (getNbMaxOperations() - 1);
				getDerniereOperation(i) == \old(getDerniereOperation(i + 1)));
	  @ ensures \old(getNbOperations()) == getNbMaxOperations()
	  		==> getSoldeAnterieur() == \old(getSoldeAnterieur() + getDerniereOperation(0));
	  @*/
	public void debiter(double debit) {
	}


	/**
	 *  Renvoie le nombre d'opérations effectuées depuis la création du compte si
	 *  ce nombre est inférieur au nombre maximal d'opérations (excepté, peut-être,
	 *  dans le cas ou le nombre maximal d'opérations mémorisées a été augmenté).
	 *  Sinon c'est le nombre maximal d'opérations qui est renvoyé.
	 *
	 * @return    Le nombre d'opérations effectuées depuis la création du compte
	 */
	//@ pure
	public int getNbOperations() {
	}


	/**
	 *  Renvoie le nombre maximal d'opérations qu'il est possible de mémoriser pour
	 *  ce compte.
	 *
	 * @return    le nombre maximal d'opérations qu'il est possible de mémoriser
	 */
	//@ pure
	public int getNbMaxOperations() {
	}


	/**
	 *  Augmente le nombre maximal d'opérations mémorisables de la valeur transmise
	 *  en paramètre. .
	 *
	 * @param  increment  Nombre d'opérations supplémentaires &agrave; mémoriser
	 */
	/*@
	  @ requires increment > 0;
	  @ ensures getNbMaxOperations() == \old(getNbMaxOperations()) + increment;
	  @ ensures (\forall int i; i >= 0 && i < getNbOperations();
				getDerniereOperation(i) == \old(getDerniereOperation(i)));
	  @*/
	public void augmenterNbMaxOperations(int increment) {
	}


	/**
	 *  Renvoie l'opération de rang index parmi les opérations effectuées sur le
	 *  compte et mémorisées. Les opérations les plus anciennes sont celles dont le
	 *  rang est le plus petit.
	 *
	 * @param  index  Rang d'une opération mémorisée
	 * @return        La valeur de l'opération mémorisée de rang index
	 */
	/*@
	  @ requires index >= 0 && index < getNbOperations();
	  @ pure
	  @*/
	public double getDerniereOperation(int index) {
	}


	/**
	 *  Renvoie un tableau de taille getNbOperations() contenant les
	 *  getNbOperations() dernières opérations effectuées sur le compte (excepté,
	 *  peut-être, dans le cas ou le nombre maximal d'opérations mémorisées a été
	 *  augmenté). Les opérations sont triées selon l'ordre dans lequel les
	 *  opérations ont été effectuées : les opérations les plus anciennes étant
	 *  placées aux indices bas du tableau (i.e. l'opération mémorisée la plus
	 *  ancienne est &agrave; l'indice 0) et les opérations les plus récentes étant
	 *  placées vers la fin du tableau.
	 *
	 * @return    Tableau de taille getNbOperations() contenant les dernières
	 *      opérations effectuées
	 */
	/*@
	  @ ensures \result != null;
	  @ ensures \result.length == getNbOperations();
	  @ ensures (\forall int i; i >= 0 && i < getNbOperations();
	  		\result[i] == getDerniereOperation(i));
	  @ pure
	  @*/
	public double[] getDernieresOperations() {
	}
}