package crous;

/** Une carte Crous possedant un montant, un nombre de points de
 * fidelite, et la categorie de son possesseur. 
 * @author M. Nebut
 * @version 11/06
*/
public class CarteCrous {
    /*@ public invariant nbPoints >= 0 && nbPoints <= DonneesCrous.maxPoints;
      @ invariant montant >= 0 && montant <= DonneesCrous.maxMontant;
      @ invariant cat != null;
      @ invariant id != null; 
      @*/

    private /*@ spec_public @*/ int nbPoints;
    private /*@ spec_public @*/ int montant;
    private /*@ spec_public @*/ Categorie cat;

    private /*@ spec_public @*/ String id;

    /*@ requires id != null;
      @ requires id.length() == 6;
      @ requires c != null;
      @
      @ ensures this.montant == 0;
      @ ensures this.nbPoints == 0;
      @ ensures this.id.equals(id);
      @ ensures this.id.length() == 6;
      @ ensures this.cat.equals(c);
      @*/
    public CarteCrous(String id, Categorie c)
    {
	this.nbPoints = 0;
	this.montant = 0;
	this.id = id;
	this.cat = c;
    }

    /** Retourne le nombre de points accumules sur cette carte. */

    /*@ ensures \result == nbPoints; 
      @*/
    public /*@ pure @*/ int getPoints() {
	return nbPoints;
    }

    /** Retourne le montant de cette carte. */
    /*@ ensures \result == montant; @*/
    public /*@ pure @*/ float getMontant() {
	return montant;
    }
    
    /** Retourne la categorie du possesseur de cette carte. */
    /*@ ensures \result == cat; @*/
    public /*@ pure @*/ Categorie getCategorie() {
	return cat;
    }


    /** Credite cette carte du montant passe en parametre.
     * @param m le montant a crediter sur cette carte.
     */
    /*@ requires m > 0;
      @ requires montant + m <= DonneesCrous.maxMontant;
      @
      @ assignable montant;
      @
      @ ensures montant == \old(montant) + m;
      @*/
    public void crediterMontant(float m) {
	montant += m;
    }

    /** Debite cette carte du montant passe en parametre.
     * @param m le montant a debiter sur cette carte.
     */
    /*@ requires m > 0;
      @ requires montant - m >= 0;
      @
      @ assignable montant;
      @
      @ ensures montant == \old(montant) - m; 
      @*/
    public void debiterMontant(float m) {
	montant -= m;
    }

    /** Ajoute sur cette carte le nombre de points passe en parametre
     * au nombre de points deja accumule.
     * @param p le nombre de points a ajouter a cette carte.
     */
    /*@ requires p > 0;
      @ requires (nbPoints + p) <= DonneesCrous.maxMontant;
      @
      @ assignable nbPoints;
      @
      @ ensures nbPoints == \old(nbPoints) + p;
      @*/
    public void crediterPoints(int p) {
	nbPoints += p;
    }

    /** Deduit sur cette carte le nombre de points passe en parametre
     * du nombre de points deja accumule.
     * @param p le nombre de points a deduire sur cette carte.
     */
    /*@ requires p > 0;
      @ requires (nbPoints - p) >= 0;
      @
      @ assignable nbPoints;
      @
      @ ensures nbPoints == \old(nbPoints) - p;
      @*/
    public void debiterPoints(int p) {
	nbPoints -= p;
    }

    /** Comparaison des id. */
    /*@ also
      @ ensures \result <==> o instanceof CarteCrous && this.id.equals(((CarteCrous) o).id);
      @
      @ signals_only \nothing;
      @*/
    public /*@ pure @*/ boolean equals(/*@ nullable @*/ Object o) {
	try {
	    CarteCrous c = (CarteCrous)o;
	    return this.id.equals(c.id);

	} catch(ClassCastException e) {
	    return false;
	} catch(NullPointerException e) {
	    return false;
	}
    }

    /*@ also
      @ ensures \result != null; 
      @*/
    public String toString() {
	return id;
    }


    /********* MAIN **************/
    public static void main(String args[])
    {
	
	CarteCrous x;
	//x = new CarteCrous("plop6", Categorie.passager);

	x = new CarteCrous("plop65", Categorie.passager); // OK

	// Credits
	//x.crediterMontant(-1);
	//x.crediterMontant(0);
	//x.crediterMontant(DonneesCrous.maxMontant + 1);
	x.crediterMontant(30); // OK

	//x.crediterPoints(-1);
	//x.crediterPoints(0);
	//x.crediterPoints(DonneesCrous.maxPoints + 1);
	x.crediterPoints(20); // OK

	// Debits
	//x.debiterPoints(-1);
	//x.debiterPoints(0);
	x.debiterPoints(20); // OK => 0

	//x.debiterMontant(0);
	//x.debiterMontant(-1);
	x.debiterMontant(30); // OK => 0
    }
}