crous
Class MachineCrous

java.lang.Object
  crous.MachineCrous

public class MachineCrous

extends java.lang.Object

Machine servant a payer un repas dans les points de restauration Crous.

Class Specifications

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  CarteCrous	carte

 

Constructor Summary

MachineCrous()           Constructeur

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
boolean	aCarte()           retourne vrai si la machine a une carte associee.
CarteCrous	getCarte()           Retourne la carte associee a la machine.
static void	main(java.lang.String[] args)
void	payerRepas()           Debite un repas sur la carte associee a la machine.
void	payerRepasGratuit()           Effectue un paiement de repas gratuit sur la carte posee sur le capteur.
float	prixRepas(Categorie c)           Retourne le prix d'un repas pour la categorie passee en parametre.
void	setCarte(CarteCrous c)           Positionne a la carte passee en parametre la carte associee a cette machine.
java.lang.String	toString()
void	unsetCarte()           La machine n'a plus de carte associee.

 

Methods inherited from class java.lang.Object

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

 

Field Detail

carte

private CarteCrous carte

Specifications: spec_public nullable

MachineCrous

public MachineCrous()

Constructeur

Specifications:

ensures this.carte == null;

aCarte

public boolean aCarte()

retourne vrai si la machine a une carte associee.

Specifications: pure

getCarte

public CarteCrous getCarte()
                    throws CarteNonPresente

Retourne la carte associee a la machine.

Throws:

CarteNonPresente

Specifications: pure

signals_only crous.CarteNonPresente;
signals (crous.CarteNonPresente) !this.aCarte();
ensures \result != null;

setCarte

public void setCarte(CarteCrous c)
              throws CarteDejaPresente

Positionne a la carte passee en parametre la carte associee a cette machine.

Parameters:

c - la carte associee a la machine

Throws:

CarteDejaPresente

Specifications:

requires c != null;
signals_only crous.CarteDejaPresente;
signals (crous.CarteDejaPresente) this.aCarte();
assignable this.carte;
ensures this.carte == c;

unsetCarte

public void unsetCarte()
                throws CarteNonPresente

La machine n'a plus de carte associee.

Throws:

CarteNonPresente

Specifications:

assignable this.carte;
signals_only crous.CarteNonPresente;
signals (crous.CarteNonPresente) !this.aCarte();
ensures this.carte == null;

prixRepas

public float prixRepas(Categorie c)
                throws CategorieInconnue

Retourne le prix d'un repas pour la categorie passee en parametre.

Parameters:

c - la categorie dont on veut le prix d'un repas

Returns:

le prix d'un repas pour la categorie c

Throws:

CategorieInconnue - s'il n'y a pas de categorie correspondante

Specifications: pure

requires c != null;
signals_only crous.CategorieInconnue;
signals (crous.CategorieInconnue) c != crous.Categorie.P1&&c != crous.Categorie.passager;
ensures \result > 0.0;

payerRepas

public void payerRepas()
                throws CarteNonPresente,
                       CreditInsuffisant,
                       CategorieInconnue

Debite un repas sur la carte associee a la machine. Credite la carte du nombre de points correspondants, dans la limite du plafond.

Throws:

CarteNonPresente

CreditInsuffisant

CategorieInconnue

Specifications:

signals_only crous.CarteNonPresente, crous.CreditInsuffisant, crous.CategorieInconnue;
signals (crous.CarteNonPresente) !this.aCarte();
signals (crous.CreditInsuffisant) this.carte.getMontant()-this.prixRepas(this.carte.getCategorie()) < 0.0;

payerRepasGratuit

public void payerRepasGratuit()
                       throws CarteNonPresente,
                              CreditInsuffisant

Effectue un paiement de repas gratuit sur la carte posee sur le capteur.

Throws:

CarteNonPresente

CreditInsuffisant

Specifications:

signals_only crous.CarteNonPresente, crous.CreditInsuffisant;
signals (crous.CarteNonPresente) !this.aCarte();
signals (crous.CreditInsuffisant) (this.carte.getPoints()-100) < 0;

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)