001 /**
002 * <code>Date</code> represente une date dans le calendrier gregorien.
003 *
004 * @author <a href="mailto:cregut@enseeiht.fr">Xavier Cregut</a>
005 * @author <a href="mailto:garion@supaero.fr">Christophe Garion</a>
006 * @version 1.0
007 */
008 public class Date {
009
010 // La date specifiee par le jour, le mois et l'annee doit toujours etre
011 // valide.
012 //@ public invariant estValide(getJour(), getMois(), getAnnee());
013
014 /**
015 * <code>jour</code> est le jour de la date.
016 *
017 */
018 private int jour;
019
020 /**
021 * <code>mois</code> est le mois de la date.
022 *
023 */
024 private int mois;
025
026 /**
027 * <code>annee</code> est l'annee de la date.
028 *
029 */
030 private int annee;
031
032 /**
033 * <code>nbJoursMois</code> est une constante representant le nombre de jours
034 * d'un mois. Le nombre de jours du mois i est joursValide[i-1].
035 * <br>On ne tient pas compte des annees bissextiles pour l'instant.
036 *
037 */
038 private static final int[] nbJoursMois = {31, 28, 31, 30, 31, 30, 31,
039 31, 30, 31, 30, 31};
040
041 /**
042 * Cumul des jours des mois precedents. <code>cumulJoursMois[i]</code> est
043 * le nombre cumule des jours des mois dont les numeros sont dans l'intervalle
044 * 1..i-1.
045 */
046 private static int cumulJoursMois[] =
047 { 0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334 };
048
049 /**
050 * Cree une nouvelle instance de <code>Date</code>.
051 *
052 * @param j un <code>int</code> qui est le jour
053 * @param m un <code>int</code> qui est le mois
054 * @param a un <code>int</code> qui est l'annee
055 */
056 //@ requires estValide(j, m, a);
057 //@ ensures getJour() == j;
058 //@ ensures getMois() == m;
059 //@ ensures getAnnee() == a;
060 public Date(int j, int m, int a) {
061 this.jour = j;
062 this.mois = m;
063 this.annee = a;
064 }
065
066 /**
067 * Modifie la date a partir du jour, du mois et de l'annee.
068 *
069 * @param j un <code>int</code> qui est le jour
070 * @param m un <code>int</code> qui est le mois
071 * @param a un <code>int</code> qui est l'annee
072 */
073 //@ requires estValide(j, m, a);
074 //@ ensures getJour() == j;
075 //@ ensures getMois() == m;
076 //@ ensures getAnnee() == a;
077 public void setDate(int j, int m, int a) {
078 this.jour = j;
079 this.mois = m;
080 this.annee = a;
081 }
082
083 /**
084 * La valeur de <code>jour</code>
085 *
086 * @return le jour
087 */
088 //@ ensures \result > 1;
089 //@ ensures \result <= nbJoursDansMois(getMois(), getAnnee());
090 public /*@ pure @*/ int getJour() {
091 return this.jour;
092 }
093
094 /**
095 * La valeur de <code>mois</code>
096 *
097 * @return le mois
098 */
099 //@ ensures \result > 0;
100 //@ ensures \result <= 12;
101 public /*@ pure @*/ int getMois() {
102 return this.mois;
103 }
104
105 /**
106 * La valeur de <code>annee</code>
107 *
108 * @return l'annee
109 */
110 //@ ensures \result > 0;
111 public /*@ pure @*/ int getAnnee() {
112 return this.annee;
113 }
114
115 /**
116 * <code>estBissextile</code> permet de savoir si une annee est bissextile.
117 *
118 * @param a un <code>int</code> qui represente une annee
119 * @return un <code>boolean</code> qui est <code>true</code> si l'annee est
120 * bissextile
121 */
122 public /*@ pure @*/ static boolean estBissextile(int a) {
123 return ((a % 4) == 0) // divisible par 4
124 && ((a % 100 != 0) // et non divible par 100
125 || (a % 400 == 0)); // sauf si divisible par 400
126 }
127
128 /**
129 * Nombre de jours dans le mois m de l'annee a.
130 *
131 * @param m un <code>int</code> qui represente le numero du mois
132 * @param a un <code>int</code> qui represente l'annee
133 * @return le nombre de jours dans le mois m de l'annee a
134 */
135 public /*@ pure @*/ static int nbJoursDansMois(int m, int a) {
136 int resultat = nbJoursMois[m-1]; // nb de jours dans le mois
137 if (m == 2 && estBissextile(a)) { // cas du mois de fevrier
138 resultat++;
139 }
140 return resultat;
141 }
142
143 /**
144 * Est-ce que l'annee est valide ?
145 *
146 * @param a un <code>int</code> qui est l'annee a verifier
147 * @return un <code>boolean</code> qui est <code>true</code> si l'entier
148 * representant l'annee est strictement positif
149 */
150 private /*@ pure @*/ static boolean estAnneeValide(int a) {
151 return (a > 0);
152 }
153
154 /**
155 * Est-ce que le mois est valide ?
156 *
157 * @param m un <code>int</code> qui represente le mois a verifier
158 * @return un <code>boolean</code> qui est <code>true</code> si le mois est
159 * bien compris entre 0 et 12
160 */
161 private /*@ pure @*/ static boolean estMoisValide(int m) {
162 return ((m > 0) && (m <=12 ));
163 }
164
165 /**
166 * Est-ce que le numero de jour j est valide pour le mois m de l'annee a ?
167 *
168 * @param j un <code>int</code> qui represente le numero du jour dans le mois m
169 * @param m un <code>int</code> qui represente le numero du mois
170 * @param a un <code>int</code> qui represente l'annee
171 */
172 private /*@ pure @*/ static boolean estJourValide(int j, int m, int a) {
173 return estAnneeValide(a) && 1 <= j && j <= nbJoursDansMois(m, a);
174 }
175
176 /**
177 * Est-ce que la date est valide ?
178 *
179 * @param j un <code>int</code> qui represente le jour
180 * @param m un <code>int</code> qui represente le mois
181 * @param a un <code>int</code> qui represente l'annee
182 * @return un <code>boolean</code> qui est true si la date est valide
183 */
184 public /*@ pure @*/ static boolean estValide(int j, int m, int a) {
185 return estAnneeValide(a) && estMoisValide(m) && estJourValide(j, m, a);
186 }
187
188 /**
189 * <code>equals</code> permet de verifier l'egalite logique entre deux dates.
190 *
191 * @param autre une <code>Date</code> a comparer a la date courante
192 * @return un boolean
193 */
194 //@ ensures \result == ((getJour() == autre.getJour()) && (getMois() == autre.getMois()) && (getAnnee() == autre.getAnnee()));
195 public /*@ pure @*/ boolean equals(Date autre) {
196 return ((getJour() == autre.getJour()) &&
197 (getMois() == autre.getMois()) &&
198 (getAnnee() == autre.getAnnee()));
199 }
200
201 /**
202 * Nombres de jours depuis l'an 0.
203 *
204 * @return nombres de jours depuis l'an 0.
205 */
206 public /*@ pure @*/ int getNbJoursDepuisAn0() {
207 int a = getAnnee() - 1; // nb d'annees pleines
208 int quantieme = getJour() // nb de jours dans le mois en cours
209 + cumulJoursMois[getMois()-1]; // nb de jours des mois precedents
210 // Prendre en compte le cas de l'annee bissextile
211 if (getMois() > 2 && estBissextile(getAnnee())) {
212 quantieme++;
213 }
214
215 return quantieme // nb de jours dans l'annee en cours
216 + 365 * a // annees considerees non bissextiles
217 + (a / 4 - a / 100 + a / 400); // nb d'annees bissextiles
218 }
219
220 /**
221 * <code>augmenter</code> permet d'augmenter la date d'un certain nombre de jours.
222 *
223 * @param nbJours le nombre de jours a incrementer
224 */
225 //@ requires nbJours > 0;
226 //@ ensures getNbJoursDepuisAn0() == \old(getNbJoursDepuisAn0()) + nbJours;
227 public void augmenter(int nbJours) {
228 // on fait n'importe quoi...
229 this.jour = this.jour + 3;
230 }
231
232 public String toString() {
233 return getJour() + "/" + getMois() + "/" + getAnnee();
234 }
235 }
|