Class Date

java.lang.Object
  Date

public class Date

extends java.lang.Object

Date represente une date dans le calendrier gregorien.

Class Specifications

public invariant estValide(this.getJour(),this.getMois(),this.getAnnee());

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

 

Constructor Summary

Date(int j, int m, int a)           Cree une nouvelle instance de Date.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	augmenter(int nbJours)           augmenter permet d'augmenter la date d'un certain nombre de jours.
boolean	equals(Date autre)           equals permet de verifier l'egalite logique entre deux dates.
static boolean	estBissextile(int a)           estBissextile permet de savoir si une annee est bissextile.
static boolean	estValide(int j, int m, int a)           Est-ce que la date est valide ?
int	getAnnee()           La valeur de annee
int	getJour()           La valeur de jour
int	getMois()           La valeur de mois
int	getNbJoursDepuisAn0()           Nombres de jours depuis l'an 0.
static int	nbJoursDansMois(int m, int a)           Nombre de jours dans le mois m de l'annee a.
void	setDate(int j, int m, int a)           Modifie la date a partir du jour, du mois et de l'annee.
java.lang.String	toString()

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

Date

public Date(int j,
            int m,
            int a)

Cree une nouvelle instance de Date.

Parameters:

j - un int qui est le jour

m - un int qui est le mois

a - un int qui est l'annee

Specifications:

requires estValide(j,m,a);
ensures this.getJour() == j;
ensures this.getMois() == m;
ensures this.getAnnee() == a;

setDate

public void setDate(int j,
                    int m,
                    int a)

Modifie la date a partir du jour, du mois et de l'annee.

Parameters:

j - un int qui est le jour

m - un int qui est le mois

a - un int qui est l'annee

Specifications:

requires estValide(j,m,a);
ensures this.getJour() == j;
ensures this.getMois() == m;
ensures this.getAnnee() == a;

getJour

public int getJour()

La valeur de jour

Returns:

le jour

Specifications: pure

ensures \result > 1;
ensures \result <= nbJoursDansMois(this.getMois(),this.getAnnee());

getMois

public int getMois()

La valeur de mois

Returns:

le mois

Specifications: pure

ensures \result > 0;
ensures \result <= 12;

getAnnee

public int getAnnee()

La valeur de annee

Returns:

l'annee

Specifications: pure

ensures \result > 0;

estBissextile

public static boolean estBissextile(int a)

estBissextile permet de savoir si une annee est bissextile.

Parameters:

a - un int qui represente une annee

Returns:

un boolean qui est true si l'annee est bissextile

Specifications: pure

nbJoursDansMois

public static int nbJoursDansMois(int m,
                                  int a)

Nombre de jours dans le mois m de l'annee a.

Parameters:

m - un int qui represente le numero du mois

a - un int qui represente l'annee

Returns:

le nombre de jours dans le mois m de l'annee a

Specifications: pure

estValide

public static boolean estValide(int j,
                                int m,
                                int a)

Est-ce que la date est valide ?

Parameters:

j - un int qui represente le jour

m - un int qui represente le mois

a - un int qui represente l'annee

Returns:

un boolean qui est true si la date est valide

Specifications: pure

equals

public boolean equals(Date autre)

equals permet de verifier l'egalite logique entre deux dates.

Parameters:

autre - une Date a comparer a la date courante

Returns:

un boolean

Specifications: pure

ensures \result == ((this.getJour() == autre.getJour())&&(this.getMois() == autre.getMois())&&(this.getAnnee() == autre.getAnnee()));

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 ;

getNbJoursDepuisAn0

public int getNbJoursDepuisAn0()

Nombres de jours depuis l'an 0.

Returns:

nombres de jours depuis l'an 0.

Specifications: pure

augmenter

public void augmenter(int nbJours)

augmenter permet d'augmenter la date d'un certain nombre de jours.

Parameters:

nbJours - le nombre de jours a incrementer

Specifications:

requires nbJours > 0;
ensures this.getNbJoursDepuisAn0() == \old(this.getNbJoursDepuisAn0())+nbJours;

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

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;