/**
* Copyright (c) 1999 GEMPLUS group. All Rights Reserved.
*------------------------------------------------------------------------------
* Project name: PACAP - cas d'étude -
*
*
* Platform : Java virtual machine
* Language : JAVA 1.1.x
* Devl tool : Symantec VisualCafe
*
* Original author: Thierry Bressure
*------------------------------------------------------------------------------
*/
package com.gemplus.pacap.utils;
/**
* Classe qui modélise une année. Les années sont comptées à partir de 1900.
* Cette classe n'est utilisée que pour valider la correction d'une année.
* Une année est correcte si son ordinal est compris entre
* Annee.MIN
et Annee.MAX
.
*/
public abstract class Annee extends Object{
//////////////// ATTRIBUTS ////////////////
/** le logiciel étant implémenter en 1999, cette année sera l'année
* minimum
*/
// modified by Nestor CATANO COLLAZOS 07/05/01
// variable modifier `final' added
// see 'Formal specification of Gemplus' electronic purse case study',
// N. Catano and M. Huisman, Section 4
public static final byte MIN = (byte)99;
/** Année maximum qui nous est imposée par la magnitude de l'octet
* en Java
*/
// code modifies by Nestor CATANO COLLAZOS 07/05/01
// variable modifier `final' added
// see 'Formal specification of Gemplus' electronic purse case study',
// N. Catano and M. Huisman, Section 4
public static final byte MAX = (byte)127;
/////////////// CONSTRUCTEUR ////////////////
//////////////// METHODES ///////////////
/*@
//modifies \nothing ;
requires true ;
ensures \result == (j >= MIN && j <= MAX) ;
//exsures (RuntimeException)false ;
*/
public static boolean check(byte j) {
return ((j >= Annee.MIN) && (j <= Annee.MAX));
}
}