Example:
*
* WayDate aDate = new WayDate(12, 22, 1998);
*
*
* @param month month of the date (month inset range(1, 12))
* @param day day of the date (day inset range(1, 31))
* @param year year of the date (year inset range(MINYEAR, MAXYEAR))
*
*/
public WayDate(int month, int day, int year)
{
assert checkValidDate(month, day, year): "Invalid date";
date = new WayDateDisplay(month, day, year);
return;
}
/**
* Return an instance of WayDate the day of the year of which
* corresponds to the input to this constructor. This constructor and the
* accessors getDayOfYear() and getYear() provide the capability to work
* with day of year (or Julian date) calculations.
*
* Example:
*
* WayDate date = new WayDate(dayYear, yr);
*
* @param dayYear day of the year for the date (dayYear inset range(1, daysInYear(year)))
* @param year year of the date (year inset range(MINYEAR, MAXYEAR))
*/
public WayDate(int dayYear, int year)
{
assert isValidYear(year) : "Illegal year: " + year;
assert isValidDayOfYear(dayYear, year) :
"Illegal day of year " + dayYear;
date = new WayDateDisplay(dayYear, year);
}
//------------------------------------------------------------------------------
// Static Methods
//------------------------------------------------------------------------------
/**
* A factory method to create an instance of WayDate with today's date.
*
* Example:
*
* WayDate date = WayDate.today();
*
* @return an instance of WayDate with the current date.
*/
public static WayDate today()
{
WayDateDisplay dt = (WayDateDisplay) WayDateImpl.today();
return new WayDate(dt.getMonth(), dt.getDay(), dt.getYear());
}
/**
* Return an instance of WayDate corresponding to a Date object.
*
* @param date an instance of the Java Date class
* @return an instance of WayDate corresponding to to the input
*/
public static WayDate asWayDate(Date date)
{
WayDateDisplay dt = (WayDateDisplay) WayDateImpl.asWayDate(date);
return new WayDate(dt.getMonth(), dt.getDay(), dt.getYear());
}
/**
* Check if a date is valid.
*
* Example:
*
* if (WayDate.checkValidDate(12, 22, 1945))
* {
* ...
* }
*
*
* @param month the month part of the date (mnth inset range(1, 12))
* @param day the day part of the date (dy inset range(1, daysInMonth(mnth, yr)))
* @param year the year part of the date (yr inset range(MINYEAR, MAXYEAR))
* @return true if the date inputs are valid
*/
public static boolean checkValidDate(int month, int day, int year)
{
boolean result;
if (!isValidYear(year))
{
result = false;
}
else if (!isValidMonth(month))
{
result = false;
}
else if (!isValidDay(month, day, year))
{
result = false;
}
else result = true;
return result;
}
/**
* Return true if the year is valid.
*
* Example:
*
* if (isValidYear(year)
* {
* . . .
* }
*
*
* @return year inset range(MINYEAR, MAXYEAR)
* @param year the year of a date
*/
static public boolean isValidYear(int year)
{
boolean result;
if ((year >= MINYEAR) && (year <= MAXYEAR)) result = true;
else result = false;
return result;
}
/**
* Return true if month is inset range(1, 12)
*
* @return month inset range(1, 12)
* @param month the month of a date
*/
static public boolean isValidMonth(int month)
{
boolean result;
if ((month >= 1) && (month <= 12)) result = true;
else result = false;
return result;
}
/**
* Return true if day inset range(1, dayOfMonth(month, year))
*
* @return day inset range(1, dayOfMonth(month, year))
* @param month the month of the date
* @param day the day of the date
* @param year the year of the date
*/
public static boolean isValidDay(int month, int day, int year)
{
boolean result;
if (!isValidYear(year) ) result = false;
else if (!isValidMonth(month)) result = false;
else if ((day >= 1) && (day <= daysInMonth(month, year))) result = true;
else result = false;
return result;
}
/**
* Return true if the day of the year is valid.
*
* @param dayOfYear the day of the year
* @param year the year
* @return dayOfYear inset range(1, daysInYear(year))
*/
public static boolean isValidDayOfYear(int dayOfYear, int year)
{
boolean result;
if (!isValidYear(year)) result = false;
else if ((dayOfYear >= 1) && (dayOfYear <= daysInYear(year))) result = true;
else result = false;
return result;
}
/**
* Return true if the day of the week is valid.
*
* @param dayOfWeek the day of the week
* @return dayOfWeek inset range(0, 6)
*/
public static boolean isValidDayOfWeek(int dayOfWeek)
{
boolean result;
if ((dayOfWeek >= SUNDAY )
&&
(dayOfWeek <= SATURDAY)
)
{
result = true;
}
else result = false;
return result;
}
/**
* Return the number of days in a month.
*
* Example:
*
* int days = date.daysInMonth(mnth, yr);
*
*
* @return the number of days in the month
* @param mnth month (month inset range(1, 12))
* @param yr year (used to determine if this is a leap year)
* (year inset range(MINYEAR, MAXYEAR))
*/
public static int daysInMonth(int mnth, int yr)
{
int dy;
assert isValidYear(yr) : "Invalid year: " + yr;
assert isValidMonth(mnth) : "Invalid month: " + mnth;
dy = WayDateImpl.daysInMonth(mnth, yr);
return dy;
}
/**
* Return true if year is a leap year
*
* Example:
*
* if (WayDate.isLeapYear(yr))
* {
* }
*
* @return result true if year is leap year
* false if year is not leap year
* @param yr a year (year inset range(MINYEAR, MAXYEAR))
*/
public static boolean isLeapYear(int yr)
{
assert isValidYear(yr) : "Illegal year: " + yr;
return WayDateImpl.isLeapYear(yr);
}
/**
* Return the number of days in a year.
*
* Example:
*
* int days = WayDate.daysInYear(yr)
*
*
* @return days number of days in the year
* @param year a year (year inset range(MINYEAR, MAXYEAR))
*
*/
public static int daysInYear(int year)
{
assert isValidYear(year) : "Illegal year: " + year;
return WayDateImpl.daysInYear(year);
}
/**
* Return a string with the abbreviated name of the month.
*
* Example:
*
* String name = WayDate.monthString(12);
*
* @return name a string with the abbreviated name of the month
* @param month the desired month (month inset range(1, 12))
*/
public static String monthString(int month)
{
assert isValidMonth(month) : "Illegal month: " + month;
return WayDateImpl.monthString(month);
}
//------------------------------------------------------------------------------
// Display interface
//------------------------------------------------------------------------------
/**
* Return the day part of the date.
*
* Example:
*
* int day = aDate.getDay();
*
* @return the day part of the date
*/
public int getDay()
{
WayDateDisplay dt = date.asWayDateDisplay();
date = dt;
return dt.getDay();
}
/**
* Return the month part of the date.
*
* Example:
*
* int month = aDate.getMonth();
*
* @return month month part of the date.
*/
public int getMonth()
{
WayDateDisplay dt = date.asWayDateDisplay();
date = dt;
return dt.getMonth();
}
/**
* Return the year part of the date.
*
* Example:
*
* int year = aDate.getYear();
*
* @return year the year part of the date.
*/
public int getYear()
{
WayDateDisplay dt = date.asWayDateDisplay();
date = dt;
return dt.getYear();
}
/**
* Return the day of the year for a particular date.
*
* Example:
*
* dayOfYear = date.getDayOfYear();
*
*
* @return dayOfYear the number of the day in the year
*
*/
public int getDayOfYear()
{
WayDateDisplay dt = date.asWayDateDisplay();
date = dt;
return dt.getDayOfYear();
}
/**
* Return true if the date is in a leap year.
* Example:
*
* if (date.isLeapYear())
* {
* }
*
*
* @return true if date is in a leap year
*/
public boolean isLeapYear()
{
WayDateDisplay dt = date.asWayDateDisplay();
date = dt;
return dt.isLeapYear();
}
//------------------------------------------------------------------------------
// Calculation interface
//------------------------------------------------------------------------------
/**
* Add a number of days to a date.
*
* Example:
*
* aDate.add(10);
*
* @param value number of days to add to the date
* @exception WayDateException thrown if result is out of bounds
*/
public void add(int value) throws WayDateException
{
WayDateCalc dt = date.asWayDateCalc();
dt.add(value);
date = dt;
return;
}
/**
* Increases the date by one day.
*
* Example:
*
* aDate.increment();
*
*/
public void increment()
{
assert !equals(MaxDate): "Date is maximum date: " + toString();
WayDateCalc dt = date.asWayDateCalc();
dt.increment();
date = dt;
return;
}
/**
* Decrement date.
*
* Example:
*
* aDate.decrement();
*
*/
public void decrement()
{
assert !equals(MinDate) : "Date is maximum date: " + toString();
WayDateCalc dt = date.asWayDateCalc();
dt.decrement();
date = dt;
}
/**
* Subtract two dates and return the number of
* days between the two.
*
* Example:
*
* diff = aDate.difference(anotherDate);
*
* @return diff an integer representing the number of days between the dates.
* @param aDate a date
*/
public int difference(WayDate aDate)
{
WayDateCalc dt = date.asWayDateCalc();
date = dt;
return dt.difference(aDate);
}
/**
* Return the day of the week as an integer.
*
* Example:
*
* dayOfWk = date.getDayOfWeek();
*
* @return dayOfWk 0 for Sunday, 1 for Monday, etc.
* (dayOfWk inset range(0, 6))
*
*/
public int getDayOfWeek()
{
WayDateCalc dt = date.asWayDateCalc();
date = dt;
return dt.getDayOfWeek();
}
/**
* Return the day of the week as a string.
*
* @return a string with the day of the weekn
*/
public String getDayOfWeekString()
{
int index = getDayOfWeek();
// assert index inset range(0,6)
return namesOfDays[index];
}
/**
* Return the date as an instance of the Jave Date class.
*
* @return an instance of Date class corresponding to this date
*/
public Date asDate()
{
int month = getMonth() - 1;
int day = getDay();
int year = getYear();
Calendar calendar = Calendar.getInstance();
calendar.set(Calendar.MONTH , month);
calendar.set(Calendar.DAY_OF_MONTH, day );
calendar.set(Calendar.YEAR , year );
Date date = calendar.getTime();
return date;
}
//------------------------------------------------------------------------------
// Comparable Interface
//------------------------------------------------------------------------------
/**
* Compare a date with the current date.
* If the date is larger, return -1.
* If the date is smaller, return +1.
* If the date is equal, return 0.
*
* Example:
*
* if (date1.compareTo(date2) == 0)
* {
* ...
* }
*
* @return result -1 if less than, 0 if equal, +1 if greater than
* @param aDate an instance of WayDate
* @exception ClassCastException if aDate is not an instance of WayDate
*/
public int compareTo(Object aDate) throws ClassCastException
{
WayDate dt = (WayDate) aDate;
WayDateCalc dt2 = (dt.getDate()).asWayDateCalc();
WayDateCalc dt1 = date.asWayDateCalc();
return dt1.compareTo(dt2);
}
//------------------------------------------------------------------------------
// Object Methods
//------------------------------------------------------------------------------
/**
* Return a copy of date. The copy always has an instance WayDateDisplay
* as its implementation object. This override is necessary because
* the clone() method in Object would return a copy pointing to the
* original date implementation object.
*
* @return an instance of WayDate
*
*/
public Object clone()
{
WayDateDisplay dt = date.asWayDateDisplay();
return new WayDate(dt.getMonth(),
dt.getDay(),
dt.getYear());
}
/**
* Return a string representation of the date.
*
* Example:
*
* String date = aDate.toString();
*
* @return date a string representing the date. The format is DD-MMM-YYYY
*
*/
public String toString()
{
date = date.asWayDateDisplay();
return ((WayDateDisplay)date).toString();
}
/**
* Return true if another date is equal to this date. Two dates are
* considered equal if they both have the same month, day, and year.
* This override is necessary because two separate WayDate objects
* can be equal, but won't be identical.
*
* @return true if dates have same month, day, and year
*/
public boolean equals(Object obj)
{
boolean result;
if (obj instanceof WayDate)
{
result = (compareTo(obj) == 0);
}
else result = false;
return result;
}
/**
* Return a hash value. This method in fact returns the absolute date
* corresponding to the date. This override is necessary so that two
* separate date objects with the same month, day, and year will return
* the same hash code even though they are different objects.
*
* @return integer has code
*/
public int hashCode()
{
WayDateCalc dt = date.asWayDateCalc();
date = dt;
return dt.getAbsoluteDate();
}
//------------------------------------------------------------------------------
// Internal Methods
//------------------------------------------------------------------------------
/**
* Return the instance of WayDateImpl for this date
*
* @return an instance of the WayDate implementation
*/
protected WayDateImpl getDate()
{
return date;
}
}
//------------------------------------------------------------------------------
//Private classes
//------------------------------------------------------------------------------
/**
* This class is an abstract class that defines the interface to the WayDate
* implementation classes and permits a type declaration common to both
* subclasses.
*/
abstract class WayDateImpl implements Serializable
{
/** an array of days in months for non-leap year */
private static final int daysNonLeapYear[] =
{31,28,31,30,31,30,31,31,30,31,30,31};
/** an array of month abbreviations */
private static final String mnthAbbrev[] = { "Jan", "Feb", "Mar", "Apr",
"May", "Jun", "Jul", "Aug",
"Sep", "Oct", "Nov", "Dec"
};
/**
* Return the number of days in a month. This routine assumes month
* and year are valid. It does not check, because checking is done in
* WayDate class.
*
* Example:
*
* int days = date.daysInMonth(mnth, yr);
*
*
* @return the number of days in the month
* @param mnth month (month inset range(1, 12))
* @param yr year (used to determine if this is a leap year)
* (yr inset range(MINYEAR, MAXYEAR))
*/
public static int daysInMonth(int mnth, int yr)
{
int dy;
if (isLeapYear(yr) && (mnth == 2)) dy = 29;
else dy = daysNonLeapYear[mnth-1];
return dy;
}
/**
* Return true if year is a leap year. Routine assumes a valid year, but
* does not check for it.
*
* Example:
*
* if (WayDateImpl.isLeapYear(yr))
* {
* }
*
* @return result true if year is leap year
* false if year is not leap year
* @param yr a year (yr inset range(MINYEAR, MAXYEAR))
*
*/
public static boolean isLeapYear(int yr)
{
return ((yr % 400 == 0)
||
((yr % 4 == 0) && (yr % 100 != 0))
);
}
/**
* Return the number of days in a year. Method assumes a valid year,
* but does not check for one.
*
* Example:
*
* int days = WayDateImpl.daysInYear(yr)
*
*
* @return days number of days in the year
* @param year a year (yr inset range(MINYEAR, MAXYEAR))
*
*/
public static int daysInYear(int year)
{
int result;
if (isLeapYear(year)) result = 366;
else result = 365;
return result;
}
/**
* Return the day of the year for a particular date. Validity of the
* date is assumed, but not checked.
*
* Example:
*
* dayInYear = WayDateImpl.dayOfYear(2, 29, 2001);
*
*
* Reference:
* Dershowitz, Nachum, and Edward M. Reingold, Calendrical Calculations,
* (Cambridge, UK: Cambridge University Press, 1997) p. 36
*
* @return dayOfYear the number of the day in the year
* (dayOfYear inset range(1,...,daysInYear(yr)))
* @param mnth month part of the date (mnth inset range(1,...,12)))
* @param dy day part of the date
* (dy inset range(1,...,daysInMonth(mnth, dy, yr)))
* @param yr year part of the date (yr inset range(MINYEAR, MAXYEAR)))
* @see Proof of Code
*/
protected static int dayOfYear(int mnth, int dy, int yr)
{
int dayInYear;
dayInYear = (367*mnth - 362)/12 + dy;
if ( isLeapYear(yr) && (mnth > 2)) dayInYear -= 1;
else if (!isLeapYear(yr) && (mnth > 2)) dayInYear -= 2;
return (dayInYear);
}
/**
* Return a string with the abbreviated name of the month.
*
* Example:
*
* String name = WayDate.monthString(12);
*
* @return name a string with the abbreviated name of the month
* @param mnth the desired month (mnth inset range(1, 12})
*
*/
public static String monthString(int mnth)
{
assert WayDate.isValidMonth(mnth) : "Illegal month: " + mnth;
return mnthAbbrev[mnth-1];
}
/**
* Return an instance of WayDateDisplay with current date
* (as obtained from the computer)
*
* @return an instance of WayDateDisplay
*/
public static WayDateImpl today()
{
// get the current date and time
Date date = new Date();
return asWayDate(date);
}
/**
* Return an instance of WayDate corresponding to the instance of date
* provided as an input.
*
* @param date an instance of the Java Date class
* @return the corresponding instance of WayDate
*/
public static WayDateImpl asWayDate(Date date)
{
Calendar calendar = Calendar.getInstance();
calendar.setTime(date);
int year = calendar.get(Calendar.YEAR); //full four digit year
int month = calendar.get(Calendar.MONTH) + 1; //add one since first month is 0
int day = calendar.get(Calendar.DAY_OF_MONTH); //in set {1,...,31}
return new WayDateDisplay(month, day, year);
}
//------------------------------------------------------------------------------
// Conversion methods
//------------------------------------------------------------------------------
/**
* Return an instance of the date as a WayDateCalc object.
*
* @return an instance of WayDateCalc equal to the current object
*/
public abstract WayDateCalc asWayDateCalc();
/**
* Return an instance of the date as a WayDateDisplay object
*
* @return an instance of WayDateDisplay equal to the current object
*/
public abstract WayDateDisplay asWayDateDisplay();
}
//------------------------------------------------------------------------------
// Calculation Date Class
//------------------------------------------------------------------------------
/**
* This class performs calculations on dates. Its field consists of a
* single absolute date field that facilitates calculations. Absolute date
* calculations cannot generate integer overflow, because an absolute date
* is always positive and less than the maximum size of an int.
*
*/
class WayDateCalc extends WayDateImpl implements DateCalculation, Comparable
{
/**
* The serial verion unique identifier for this class
*/
private static final long serialVersionUID = 9701L;
/**
* The maximum absolute date for 31-DEC-3999
*/
private static final int MAX_ABSOLUTE = 876216; //absolute date for 31-DEC-3999
/**
* The absolute date
*/
private int abDate;
/**
* Given a date, return the number of days since 12/31/1600.
* Absolute dates, or the number of days from the beginning range
* of legal dates, are used to perform computations upon dates.
* Thus a date calculation can be performed by converting the
* input dates to absolute dates, performing the calculations,
* and converting the result back to a gregorian date.
*
* Example:
*
* WayDateCalc date = new WayDateCalc(month, day, year);
*
*
* @param month the month part of the date (month inset range(1, 12))
* @param day the day part of the date (day inset range(1, daysInMonth(month, year))
* @param year the year part of the date (year inset range(MINYEAR, MAXYEAR))
*/
public WayDateCalc(int month, int day, int year)
{
abDate = dayOfYear(month, day, year) + daysInPriorYears(year);
return;
}
/**
* Return the number of days in prior years.
* * The algorithm works by counting the number of days in prior years * since the beginning of 1601. Multiplying the number of years by * 365 gives an initial estimate, but underestimates the number of * days because it does not count leap days. Therefore, we add * a day for every fourth year. This over-compensates, because * some years divisible by 100 are not leap years. We therefore * subtract the years divisible by 100. But this is too much * of a correction, since years divisible by 400 are leap years. * So we finally add in the number of years divisible by 400. *
** Reference: * Edward M. Reingold and Nachum Dershowitz, Calendrical Calculations: * The Millennium Edition * (Cambridge, UK: Cambridge University Press, 2001) * p. 51 *
*Example:
*
* days = WayDate.daysInPriorYears(yr);
*
*
* @return days number of days in years prior to yr.
* @param yr a year (yr inset range(MINYEAR,...,MAXYEAR))
*
*/
protected static int daysInPriorYears(int yr)
{
assert yr >= 1601:"illegal year: " + yr;
int y = yr - 1601;
int days;
days = 365 * y // days in prior years
+ y/4 // plus julian leap days in prior years
- y/100 // minus prior century years
+ y/400; // plus years divisible by 400
return days;
}
/**
* Return the year implied by an absolute date. The algorithm is from:
*
* Edward M. Reingold and Nachum Dershowitz, Calendrical Calculations:
* The Millennium Edition
* (Cambridge, UK: Cambridge University Press, 2001)
* p. 52
*
* @return year year associated with an absolute date
* (year inset range(MINYEAR, MAXYEAR))
* @param abDate an absolute date (abDate inset range(1, MAX_ABSOLUTE})
*
*/
public static int yearFromAbsolute(int abDate)
{
int year;
int d0 = abDate - 1;
int n400 = d0/146097; //Number of days in a 400 year cycle:
// 400*365 + 100 - 3
int d1 = d0 % 146097;
int n100 = d1/36524; //Number of days in 100 year cycle:
// 365*100 + 25 - 1
int d2 = d1 % 36524;
int n4 = d2/1461; //Number of days in 4 year cycle:
// 365*4 + 1
int d3 = d2 % 1461;
int n1 = d3/365; //Number of days in 1 year:
// 365
//
// If n100 = 4 orelse n1 = 4, then the date is 31-Dec of the leap
// year so we add one less year to get the absolute year
//
if ((n100 == 4) || (n1 == 4))
year = 400*n400 + 100*n100 + 4*n4 + n1 + 1600;
else
year = 400*n400 + 100*n100 + 4*n4 + n1 + 1601;
return year;
}
//
// Conversion Methods
//
/**
* Return an instance of WayDateDisplay.
*
* @return the current object
*/
public WayDateDisplay asWayDateDisplay()
{
int year = yearFromAbsolute(abDate);
int dayOfYear = abDate - daysInPriorYears(year);
return new WayDateDisplay(dayOfYear, year);
}
/**
* Return an instance of WayDateCalc with an equivalent value.
* Since this is a WayDateCalc object, return this.
*
* @return an instance of WayDateCalc
*/
public WayDateCalc asWayDateCalc()
{
return this;
}
//
// Date Caclulation Interface
//
/**
* Add a number of days to a date.
*
* Example:
*
* aDate.add(10);
*
* @param value number of days to add to the date
*/
public void add(int value) throws WayDateException
{
int result = abDate + value;
if (result < 1)
{
throw new WayDateException(WayDateException.ILLEGAL_ABSOLUTE, result);
}
if (result > MAX_ABSOLUTE)
{
throw new WayDateException(WayDateException.ILLEGAL_ABSOLUTE, result);
}
abDate = result;
return;
}
/**
* Increases the date by one day.
*
* Example:
*
* aDate.increment();
*
*/
public void increment()
{
assert (abDate < MAX_ABSOLUTE) : "absolute date is maximum";
abDate++;
return;
}
/**
* Decrement date.
*
* Example:
*
* aDate.decrement();
*
*/
public void decrement()
{
assert (abDate > 1) : "Absolute date is 1";
abDate--;
return;
}
/**
* Subtract two dates and return the number of
* days between the two.
*
* Example:
*
* diff = aDate.difference(anotherDate);
*
* @return the number of days between the dates.
* @param anotherDate a date
*/
public int difference(WayDate anotherDate)
{
WayDateCalc date2 = anotherDate.getDate().asWayDateCalc();
return abDate - date2.getAbsoluteDate();
}
/**
* Return the day of the week as an integer. This method depends on
* the fact that 1-Jan-1601 is a Monday.
*
* Example:
*
* dayOfWk = date.getDayOfWeek();
*
* @return dayOfWk 0 for Sunday, 1 for Monday, etc.
* (dayOfWk inset range(0, 6))
*
*/
public int getDayOfWeek()
{
return abDate % 7;
}
//
// Comparable Interface
//
/**
* Compare a date with the current date.
* If the current date is less than supplied date, return -1.
* If the current date is greater than supplied date, return +1.
* If the current date is equal to supplied date, return 0.
*
* Example:
*
* if (date1.compareTo(date2) == 0)
* {
* ...
* }
*
* @return result -1 if less than, 0 if equal, +1 if greater than
* @param aDate a date
*/
public int compareTo(Object aDate)
{
int abDate2 = ((WayDateCalc)aDate).getAbsoluteDate();
int result;
if (abDate2 > abDate) {result = -1;}
else if (abDate2 < abDate) {result = 1;}
else {result = 0;}
return result;
}
//
// Internal methods
//
/**
* Return the absolute date value
*
* @return absolute date
*/
public int getAbsoluteDate()
{
return abDate;
}
}
//------------------------------------------------------------------------------
// Display Date Class
//------------------------------------------------------------------------------
/**
* This class handles displaying of dates. Its fields separately record
* the month, day, and year of the date.
*
*/
class WayDateDisplay extends WayDateImpl implements DateDisplay
{
/**
* The serial verion unique identifier for this class
*/
private static final long serialVersionUID = 9701L;
// Fields
/**
* The day portion of the date
*/
protected final int day;
/**
* The month portion of the date
*/
protected final int month;
/**
* The year portion of the date
*/
protected final int year;
/**
* Create a WayDate object with the specified
* month, day, and year.
*
* Example:
*
* WayDate aDate = new WayDate(12, 22, 1998);
*
* Specification
* * @param _month month of the date (_month inset range(1, 12)) * @param _day day of the date (_day inset range(1, daysInMonth(_month))) * @param _year year of the date (_year inset range(MINYEAR, MAXYEAR)) * */ public WayDateDisplay(int _month, int _day, int _year) { month = _month; day = _day; year = _year; } /** * Return an instance of WayDateDisplay the day of the year of which * corresponds to the input to this constructor. This constructor and the * accessors getDayOfYear() and getYear() provide the capability to work * with day of year (or Julian date) calculations. * *
Example:
*
* WayDate date = new WayDate(dayOfYear, yr);
*
* @param dayYear day of the year for the date (dayOfYear inset range(1,daysInYear(year))
* @param yr year of the date (yr inset range(MINYEAR, MAXYEAR))
*/
public WayDateDisplay(int dayYear, int yr)
{
int mnth = 1;
int dy = 1;
year = yr;
int diff = dayYear - 1; // dayOfYear(1, 1, year) = 1
/*
* Precondition: isValidYear(yr) andalso isValidDayOfYear(dayYear)
* Loop Invariant: diff = dayYear - dayOfYear(mnth, dy, yr) andalso
* mnth inset range(1, 12) andalso
* dy inset range(1, daysInMonth(mnth,yr))
*
* Bound Function:
* fun diff(dayYear : int, mnth : Month, dy : Day, year : Year) : int=
* dayYear - dayOfYear(mnth, dy, year);
*
* Termination: diff = 0
* Postcondition: dayOfYear = dayOfYear(mnth, dy, yr) andalso
* isValidDate(mnth, dy, yr)
*/
/*
* Theorem 1: Changes in dayOfYear, month > 1
*
* Precondition: month inset range(2, 12)
* Postcondition: daysInMonth(month, year) = dayOfYear(month, day, year) -
* dayOfYear(month-1, day, year)
* Proof:
* From definiton of dayOfYear()
*/
/*
* Theorem 2: Changes in dayOfYear, month = 1
*
* Precondition: month = 1 andalso day = 31
* Postcondition: daysInMonth(month, year) = dayOfYear(month, day, year)
*
* Proof:
* From definition of dayOfYear()
*/
/*
* Theorem 3: Change in day of month
*
* Precondition: diff < daysInMonth(month, year)
* Postcondition: diff = dayOfYear(month, diff + 1, year) -
* dayOfYear(month, 1, year)
*
* Proof:
* From definition of dayOfYear()
*/
/*
* Proof Obligation 1: the invariant holds at the beginning
*
* Proof:
* From: dayOfYear(1, 1, yr) = 1
* 1. diff = dayYear - dayOfYear(1, 1, yr)
* 2. 1 inset range(1, 12)
* 3. 1 inset range(1, daysInMonth(mnth,yr))
* Infer: invariant holds
*/
while (diff > 0)
{
if (diff >= daysInMonth(mnth, year))
{
diff -= daysInMonth(mnth, year);
mnth++;
/*
* Proof Obligation 2: the invariant still holds
*
* Proof:
* From: diff = diff' - daysInMonth(mnth, year)
* 1. diff = diff' -
* dayOfYear(mnth, year) + dayOfYear(mnth-1, year) {Theorem 1 and 2}
* 2. diff' = dayYear - dayOfYear(mnth-1, 1, year)
* 3. diff = dayYear - dayOfYear(mnth , 1, year)
* 4. dy = 1
* 5. mnth inset range(1, 12) {Precondition}
* Infer: diff = dayYear - dayOfYear(mnth, 1, yr) andalso
* mnth inset range(1, 12) andalso
* dy inset range(1, daysInMonth(mnth,yr))
*/
}
else
{
dy = diff + 1;
diff = 0;
/*
* Proof Obligation 2: the invariant still holds
*
* Proof:
* From: dy = diff + 1 andalso diff = 0
* 1. mnth inset range(1,12) {invariant prior iteration}
* 2. dy inset range(1, daysInMonth(mnth,yr)) {1st guard command}
* 3. diff' = dayYear - dayOfYear(mnth, 1, yr)
* 4. diff' = dayYear - dayOfYear(mnth, diff' + 1, yr) +
* diff' {Theorem 3}
* 5. 0 = dayYear - dayOfYear(mnth, dy, yr)
* 6. diff = 0
* 7. diff = dayYear - dayOfYear(mnth, dy, yr)
* Infer: diff = dayYear - dayOfYear(mnth, dy, yr) andalso
* mnth inset range(1, 12) andalso
* dy inset range(1, daysInMonth(mnth,yr))
*/
}
}
day = dy;
month = mnth;
/*
* Proof Obligation 5: Each iteration reduces bound function
*
* Proof:
* Under first guard, diff is reduced by dayInMonth which is
* always positive.
*
* Under second guard, diff is set to 0 terminating iteration
*/
/*
* Proof Obligation 4: Bound function is positive if loop has not terminated.
*
* Proof:
* diff must be positive else loop terminates
*/
/*
* Proof Obligation 3: Postcondition is true
*
* From: 0 = dayYear - dayOfYear(mnth, dy, yr) andalso
* mnth inset range(1, 12) andalso
* dy inset range(1, daysInMonth(mnth,yr))
* 1. dayYear = dayOfYear(mnth, dy, yr) andalso
* mnth inset range(1, 12) andalso
* dy inset range(1, daysInMonth(mnth, yr))
* Infer: postcondition holds
*/
return;
}
/**
* Return an instance of WayDateDisplay. Since this object is
* a WayDateDisplay, just return the current object.
*
* @return the current object
*/
public WayDateDisplay asWayDateDisplay()
{
return this;
}
/**
* Return an instance of WayDateCalc with an equivalent value.
*
* @return an instance of WayDateCalc
*/
public WayDateCalc asWayDateCalc()
{
return new WayDateCalc(month, day, year);
}
//
// Access Routines
//
/**
* Return the day part of the date.
*
* Example:
*
* int day = aDate.getDay();
*
* @return day the day part of the date
*/
public int getDay()
{
return day;
}
/**
* Return the month part of the date.
*
* Example:
*
* int month = aDate.getMonth();
*
* @return month month part of the date.
*/
public int getMonth()
{
return month;
}
/**
* Return the year part of the date.
*
* Example:
*
* int year = aDate.getYear();
*
* @return year the year part of the date.
*/
public int getYear()
{
return year;
}
/**
* Return true if the date is in a leap year.
* Example:
*
* if (date.isLeapYear())
* {
* }
*
*
* @return true if date is in a leap year
*/
public boolean isLeapYear()
{
return isLeapYear(year);
}
/**
* Return the day of the year for a date.
*
* Example:
*
* int dayYear = date.getDayOfYear();
*
* @return the day of the year for the date.
*/
public int getDayOfYear()
{
return dayOfYear(month, day, year);
}
/**
* Return a string representation of the date.
*
* Example:
*
* String date = aDate.toString();
*
* @return date a string representing the date. The format is DD-MMM-YYYY
*
*/
public String toString()
{
String dayString = String.valueOf(day);
if (dayString.length() == 1) dayString = "0" + dayString;
String dateString = dayString + "-" +
monthString(month) + "-" +
String.valueOf(year);
return dateString;
}
}