crous
Class CarteCrous

java.lang.Object
  crous.CarteCrous

public class CarteCrous

extends java.lang.Object

Une carte Crous possedant un montant, un nombre de points de fidelite, et la categorie de son possesseur.

Class Specifications

public invariant this.nbPoints >= 0&&this.nbPoints <= 1000;

Specifications inherited from class Object

public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
[spec_public] private  Categorie	cat
[spec_public] private  java.lang.String	id
[spec_public] private  int	montant
[spec_public] private  int	nbPoints

 

Constructor Summary

CarteCrous(java.lang.String id, Categorie c)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	crediterMontant(float m)           Credite cette carte du montant passe en parametre.
void	crediterPoints(int p)           Ajoute sur cette carte le nombre de points passe en parametre au nombre de points deja accumule.
void	debiterMontant(float m)           Debite cette carte du montant passe en parametre.
void	debiterPoints(int p)           Deduit sur cette carte le nombre de points passe en parametre du nombre de points deja accumule.
boolean	equals(nullable java.lang.Object o)           Comparaison des id.
Categorie	getCategorie()           Retourne la categorie du possesseur de cette carte.
float	getMontant()           Retourne le montant de cette carte.
int	getPoints()           Retourne le nombre de points accumules sur cette carte.
static void	main(java.lang.String[] args)           MAIN
java.lang.String	toString()

 

Methods inherited from class java.lang.Object

clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Field Detail

nbPoints

private int nbPoints

Specifications: spec_public

montant

private int montant

Specifications: spec_public

cat

private Categorie cat

Specifications: spec_public

id

private java.lang.String id

Specifications: spec_public

CarteCrous

public CarteCrous(java.lang.String id,
                  Categorie c)

Specifications:

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);

getPoints

public int getPoints()

Retourne le nombre de points accumules sur cette carte.

Specifications: pure

ensures \result == this.nbPoints;

getMontant

public float getMontant()

Retourne le montant de cette carte.

Specifications: pure

ensures \result == this.montant;

getCategorie

public Categorie getCategorie()

Retourne la categorie du possesseur de cette carte.

Specifications: pure

ensures \result == this.cat;

crediterMontant

public void crediterMontant(float m)

Credite cette carte du montant passe en parametre.

Parameters:

m - le montant a crediter sur cette carte.

Specifications:

requires m > 0.0;
requires this.montant+m <= 150.0;
assignable montant;
ensures this.montant == \old(this.montant)+m;

debiterMontant

public void debiterMontant(float m)

Debite cette carte du montant passe en parametre.

Parameters:

m - le montant a debiter sur cette carte.

Specifications:

requires m > 0.0;
requires this.montant-m >= 0.0;
assignable montant;
ensures this.montant == \old(this.montant)-m;

crediterPoints

public void crediterPoints(int p)

Ajoute sur cette carte le nombre de points passe en parametre au nombre de points deja accumule.

Parameters:

p - le nombre de points a ajouter a cette carte.

Specifications:

requires p > 0;
requires (this.nbPoints+p) <= 150.0;
assignable nbPoints;
ensures this.nbPoints == \old(this.nbPoints)+p;

debiterPoints

public void debiterPoints(int p)

Deduit sur cette carte le nombre de points passe en parametre du nombre de points deja accumule.

Parameters:

p - le nombre de points a deduire sur cette carte.

Specifications:

requires p > 0;
requires (this.nbPoints-p) >= 0;
assignable nbPoints;
ensures this.nbPoints == \old(this.nbPoints)-p;

equals

public boolean equals(nullable java.lang.Object o)

Comparaison des id.

Overrides:

equals in class java.lang.Object

Specifications: pure

     also

ensures \result <==> o instanceof crous.CarteCrous&&this.id.equals(((crous.CarteCrous)o).id);
signals_only \nothing;

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

Specifications:

     also

ensures \result != null;

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;

main

public static void main(java.lang.String[] args)

MAIN