java.util
Class GregorianCalendar

java.lang.Object
  java.util.Calendar
      java.util.GregorianCalendar

All Implemented Interfaces:

Cloneable, Serializable

public class GregorianCalendar

extends Calendar

JML's specification of java.util.Calendar.

Version:

$Revision: 1.20 $

Author:

Kristina Boysen, Gary T. Leavens

Class Specifications

public invariant this.zone != null; public invariant this.locale != null; public invariant this.boundsCheck(this.fields[0],0); public invariant this.boundsCheck(this.fields[1],1); public invariant this.boundsCheck(this.fields[2],2); public invariant this.boundsCheck(this.fields[3],3); public invariant this.boundsCheck(this.fields[4],4); public invariant this.boundsCheck(this.fields[5],5); public invariant this.boundsCheck(this.fields[5],5); public invariant this.boundsCheck(this.fields[6],6); public invariant this.boundsCheck(this.fields[7],7); public invariant this.boundsCheck(this.fields[8],8); public invariant this.boundsCheck(this.fields[9],9); public invariant this.boundsCheck(this.fields[10],10); public invariant this.boundsCheck(this.fields[11],11); public invariant this.boundsCheck(this.fields[12],12); public invariant this.boundsCheck(this.fields[13],13); public invariant this.boundsCheck(this.fields[14],14); public invariant this.boundsCheck(this.fields[15],15); public invariant this.boundsCheck(this.fields[16],16); public invariant this.boundsCheck(this.fields[17],17);

Specifications inherited from class Calendar

public invariant this.zone != null;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.util.Calendar

locale

 

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
static int	AD
static int	BC
[spec_public] private static int	EPOCH_JULIAN_DAY
[spec_public] private static int	EPOCH_YEAR
[spec_public] private  long	gregorianCutover
[spec_public] private  int	gregorianCutoverYear
[spec_public] private static int	JAN_1_1_JULIAN_DAY
[spec_public] private static int[]	LEAP_MONTH_LENGTH
[spec_public] private static int[]	LEAP_NUM_DAYS
[spec_public] private static int[]	LEAST_MAX_VALUES
[spec_public] private static int[]	MAX_VALUES
[spec_public] private static int[]	MIN_VALUES
[spec_public] private static int[]	MONTH_LENGTH
[spec_public] private  long	normalizedGregorianCutover
[spec_public] private static int[]	NUM_DAYS
[spec_public] private static long	ONE_DAY
[spec_public] private static int	ONE_HOUR
[spec_public] private static int	ONE_MINUTE
[spec_public] private static int	ONE_SECOND
[spec_public] private static long	ONE_WEEK
(package private) static long	serialVersionUID

 

Fields inherited from class java.util.Calendar

AM, AM_PM, APRIL, areAllFieldsSet, areFieldsSet, AUGUST, cachedLocaleData, currentSerialVersion, DATE, DAY_OF_MONTH, DAY_OF_WEEK, DAY_OF_WEEK_IN_MONTH, DAY_OF_YEAR, DECEMBER, DST_OFFSET, ERA, FEBRUARY, FIELD_COUNT, fields, firstDayOfWeek, FRIDAY, HOUR, HOUR_OF_DAY, INTERNALLY_SET, isSet, isTimeSet, JANUARY, JULY, JUNE, lenient, MARCH, MAY, MILLISECOND, minimalDaysInFirstWeek, MINIMUM_USER_STAMP, MINUTE, MONDAY, MONTH, NOVEMBER, OCTOBER, PM, SATURDAY, SECOND, SEPTEMBER, stamp, SUNDAY, THURSDAY, time, TUESDAY, UNDECIMBER, UNSET, WEDNESDAY, WEEK_OF_MONTH, WEEK_OF_YEAR, YEAR, zone, ZONE_OFFSET

 

Constructor Summary

GregorianCalendar()

GregorianCalendar(int year, int month, int date)

GregorianCalendar(int year, int month, int date, int hour, int minute)

GregorianCalendar(int year, int month, int date, int hour, int minute, int second)

GregorianCalendar(Locale aLocale)

GregorianCalendar(TimeZone zone)

GregorianCalendar(TimeZone zone, Locale aLocale)

 

Model Method Summary
boolean	calendarFieldsAreSet()           This should return true if isTimeSet and areFieldsSet are false and false if both are true.
int	computeDayOfMonth(int amount)           This should compute the new day of week after amount is added to it.
long	computeDelta(int field, int amount)           This should compute the number of milliseconds in the entered field and multiply the entered amount by that delta value.
int	computeDST(boolean adjustDST, int oldDSTOffset, int newDSTOffset)           This should compute the daylight savings time (DST) for any field that sets its adjustDST variable to true.
int	computeIsoYear()           This should return the ISO year depending on the conditions of WEEK_OF_YEAR and MONTH.
int	computeLowGood()           This should return the maximum possible value for the YEAR field, depending on the type of calendar.
long	computeMillis()           Model methods used for computeTime() This should compute the number of milliseconds from the current values of the fields without DST or time zone adjustments
long	computeMillisInDay(long millis)           This should return the number of milliseconds past midnight for for the date specified by millis.
long	computeMin2()           This should compute min2 value used for computing the roll amount for DAY_OF_WEEK.
int	computeMonth(int amount)           This should compute the new month value after amount is added to it.
int	computeNewHour(int field, int amount, Date start, int oldHour)           This should return the value by which oldHour changes once amount is added to it.
int	computeValue(int field, int amount)           This should compute the new value for which to roll field after amount is added to it.
int	computeWoy(int amount)           This should compute the new week of year value after amount is added to it.
int	computeZoneOffset(long millis)           This should return the correct time zone offset for the current time zone and the given time, specified by the argument millis.
int[]	getOffsetsForComputeFields()           This should return the number of milliseconds past midnight for for the date specified by millis.
boolean	isComplete()           This should return true if areFieldsSet and areAllFieldsSet are true, and false if both are false.
boolean	isYAmountNotZero(int month)           This should return whether the y_amount calculated in the method is zero.
boolean	milliFieldsAreSet()           This should return true if isTimeSet, areFieldsSet, and areAllFieldsSet are all true.
boolean	pinDayOfMonthIsSet(int oldDayOfMonth, int dayOfMonth)           This should return true if month value is set correctly after adjustments to higher fields.
boolean	timeToFieldsVarsAreSet()           This should return true if the isSet[field] methods all are true and if calendarFieldsAreSet() also returns true.

 

Model methods inherited from class java.util.Calendar

correspondsTimeAndFields, resultIsMaximum, resultIsMinimum

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	add(int field, int amount)
[spec_public] private  boolean	boundsCheck(int value, int field)
protected  void	computeFields()
protected  void	computeTime()
boolean	equals(nullable Object obj)
[spec_public] private static long	floorDivide(long numerator, long denominator)
int	getActualMaximum(int field)
int	getActualMinimum(int field)
int	getGreatestMinimum(int field)
Date	getGregorianChange()
(package private)  int	getISOYear()
int	getLeastMaximum(int field)
int	getMaximum(int field)
int	getMinimum(int field)
int	hashCode()
(package private)  boolean	inDaylightTime()
[spec_public] private  int	internalGetEra()
boolean	isLeapYear(int year)
[spec_public] private  int	monthLength(int month)
void	roll(int fld, boolean up)
void	roll(int field, int amount)
void	setGregorianChange(Date date)
[spec_public] private  boolean	validateFields()
[spec_public] private  int	yearLength()

 

Methods inherited from class java.util.Calendar

after, before, clear, clear, clone, complete, get, getAvailableLocales, getFirstDayOfWeek, getInstance, getInstance, getInstance, getInstance, getMinimalDaysInFirstWeek, getTime, getTimeInMillis, getTimeZone, internalGet, internalSet, isLenient, isSet, set, set, set, set, setFirstDayOfWeek, setLenient, setMinimalDaysInFirstWeek, setTime, setTimeInMillis, setTimeZone, toString

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

BC

public static final int BC

AD

public static final int AD

JAN_1_1_JULIAN_DAY

private static final int JAN_1_1_JULIAN_DAY

Specifications: spec_public

EPOCH_JULIAN_DAY

private static final int EPOCH_JULIAN_DAY

Specifications: spec_public

EPOCH_YEAR

private static final int EPOCH_YEAR

Specifications: spec_public

ONE_SECOND

private static final int ONE_SECOND

Specifications: spec_public

ONE_MINUTE

private static final int ONE_MINUTE

Specifications: spec_public

ONE_HOUR

private static final int ONE_HOUR

Specifications: spec_public

ONE_DAY

private static final long ONE_DAY

Specifications: spec_public

ONE_WEEK

private static final long ONE_WEEK

Specifications: spec_public

NUM_DAYS

private static final int[] NUM_DAYS

Specifications: spec_public

LEAP_NUM_DAYS

private static final int[] LEAP_NUM_DAYS

Specifications: spec_public

MONTH_LENGTH

private static final int[] MONTH_LENGTH

Specifications: spec_public

LEAP_MONTH_LENGTH

private static final int[] LEAP_MONTH_LENGTH

Specifications: spec_public

MIN_VALUES

private static final int[] MIN_VALUES

Specifications: spec_public

LEAST_MAX_VALUES

private static final int[] LEAST_MAX_VALUES

Specifications: spec_public

MAX_VALUES

private static final int[] MAX_VALUES

Specifications: spec_public

gregorianCutover

private long gregorianCutover

Specifications: spec_public

normalizedGregorianCutover

private transient long normalizedGregorianCutover

Specifications: spec_public

gregorianCutoverYear

private transient int gregorianCutoverYear

Specifications: spec_public

serialVersionUID

static final long serialVersionUID

GregorianCalendar

public GregorianCalendar()

Specifications:

public normal_behavior
assignable zone, locale;
ensures this.zone.equals(java.util.TimeZone.getDefault())&&this.locale.equals(java.util.Locale.getDefault());

GregorianCalendar

public GregorianCalendar(TimeZone zone)

Specifications:

public normal_behavior
requires zone != null;
assignable this.zone, locale;
ensures this.zone.equals(zone)&&this.locale.equals(java.util.Locale.getDefault());

GregorianCalendar

public GregorianCalendar(Locale aLocale)

Specifications:

public normal_behavior
requires aLocale != null;
assignable zone, locale;
ensures this.zone.equals(java.util.TimeZone.getDefault())&&this.locale.equals(aLocale);

GregorianCalendar

public GregorianCalendar(TimeZone zone,
                         Locale aLocale)

Specifications:

public normal_behavior
requires zone != null&&aLocale != null;
assignable this.zone, locale, System.clock;
assignable_redundantly time, isTimeSet, areFieldsSet, areAllFieldsSet;
ensures this.zone.equals(zone)&&this.locale.equals(aLocale);

GregorianCalendar

public GregorianCalendar(int year,
                         int month,
                         int date)

Specifications:

public normal_behavior
assignable zone, locale;
assignable_redundantly fields[1], fields[2], fields[5], isTimeSet, areFieldsSet, isSet[*];
ensures this.zone.equals(java.util.TimeZone.getDefault())&&this.locale.equals(java.util.Locale.getDefault());
ensures_redundantly this.fields[1] == year&&this.fields[2] == month&&this.fields[5] == date&&this.isSet[1]&&this.isSet[2]&&this.isSet[5]&&this.calendarFieldsAreSet();

GregorianCalendar

public GregorianCalendar(int year,
                         int month,
                         int date,
                         int hour,
                         int minute)

Specifications:

public normal_behavior
assignable zone, locale;
assignable_redundantly fields[1], fields[2], fields[5], fields[11], fields[12], isTimeSet, areFieldsSet, isSet[*];
ensures this.zone.equals(java.util.TimeZone.getDefault())&&this.locale.equals(java.util.Locale.getDefault());
ensures_redundantly this.fields[1] == year&&this.fields[2] == month&&this.fields[5] == date&&this.fields[11] == hour&&this.fields[12] == minute&&this.isSet[1]&&this.isSet[2]&&this.isSet[5]&&this.isSet[11]&&this.isSet[12]&&this.calendarFieldsAreSet();

GregorianCalendar

public GregorianCalendar(int year,
                         int month,
                         int date,
                         int hour,
                         int minute,
                         int second)

Specifications:

public normal_behavior
assignable zone, locale;
assignable_redundantly fields[1], fields[2], fields[5], fields[11], fields[12], fields[13], isTimeSet, areFieldsSet, isSet[*];
ensures this.zone.equals(java.util.TimeZone.getDefault())&&this.locale.equals(java.util.Locale.getDefault());
ensures_redundantly this.fields[1] == year&&this.fields[2] == month&&this.fields[5] == date&&this.fields[11] == hour&&this.fields[12] == minute&&this.fields[13] == second&&this.isSet[1]&&this.isSet[2]&&this.isSet[5]&&this.isSet[11]&&this.isSet[12]&&this.isSet[13]&&this.calendarFieldsAreSet();

milliFieldsAreSet

public boolean milliFieldsAreSet()

This should return true if isTimeSet, areFieldsSet, and areAllFieldsSet are all true.

Returns:

true if isTimeSet, areFieldsSet, and areAllFields set are true; false otherwise.

Specifications: pure

calendarFieldsAreSet

public boolean calendarFieldsAreSet()

This should return true if isTimeSet and areFieldsSet are false and false if both are true.

Returns:

true if isTimeSet and areFieldsSet are false; false otherwise.

Specifications: pure

isComplete

public boolean isComplete()

This should return true if areFieldsSet and areAllFieldsSet are true, and false if both are false.

Returns:

true if areFieldsSet and areAllFieldsSet are true; false otherwise.

Specifications: pure

pinDayOfMonthIsSet

public boolean pinDayOfMonthIsSet(int oldDayOfMonth,
                                  int dayOfMonth)

This should return true if month value is set correctly after adjustments to higher fields. This means that if we add 1 month to January 31st, the resulting month is set to February 28th instead of March 3rd (example from JavaDoc).

Returns:

true if month value is set correctly after adjustments to higher fields; false otherwise.

Specifications: pure

public normal_behavior
old int monthLen = this.monthLength(this.get(2));

{|

requires oldDayOfMonth > monthLen;
assignable \nothing;
ensures \result == (dayOfMonth == monthLen);

also

requires oldDayOfMonth <= monthLen;
assignable \nothing;
ensures \result == (dayOfMonth == oldDayOfMonth);

|}

isYAmountNotZero

public boolean isYAmountNotZero(int month)

This should return whether the y_amount calculated in the method is zero. This y_amount determines whether the current month plus amount is a valid value for month.

Returns:

true if the current month + amount is valid; false otherwise

Specifications: pure

public normal_behavior
old int y_amount = 0;

{|

requires y_amount != 0;
assignable \nothing;
ensures \result == true;

also

requires y_amount == 0;
assignable \nothing;
ensures \result == false;

|}

computeDelta

public long computeDelta(int field,
                         int amount)

This should compute the number of milliseconds in the entered field and multiply the entered amount by that delta value.

Returns:

the delta value for the entered field and amount

Specifications: pure

public normal_behavior
old int delta = amount;

{|

requires field == 3||field == 4||field == 8;
assignable \nothing;
ensures delta == delta*7*24*60*60*1000;

also

requires field == 9;
assignable \nothing;
ensures delta == delta*12*60*60*1000;

also

requires field == 5||field == 6||field == 7;
assignable \nothing;
ensures delta == delta*24*60*60*1000;

also

requires field == 11||field == 10;
assignable \nothing;
ensures delta == delta*60*60*1000;

also

requires field == 12;
assignable \nothing;
ensures delta == delta*60*1000;

also

requires field == 13;
assignable \nothing;
ensures delta == delta*1000;

|}

computeDST

public int computeDST(boolean adjustDST,
                      int oldDSTOffset,
                      int newDSTOffset)

This should compute the daylight savings time (DST) for any field that sets its adjustDST variable to true.

Returns:

the dst value for the given DST offsets

Specifications: pure

public normal_behavior
old int dst = 0;
requires adjustDST;
assignable \nothing;
ensures dst == oldDSTOffset-newDSTOffset;

computeLowGood

public int computeLowGood()

This should return the maximum possible value for the YEAR field, depending on the type of calendar.

Returns:

the maximum possible value for YEAR, depending on the calendar

Specifications: pure

public normal_behavior
old int lowGood = java.util.GregorianCalendar.LEAST_MAX_VALUES[1];
assignable \nothing;
ensures \result == lowGood&&java.util.GregorianCalendar.LEAST_MAX_VALUES[1] <= lowGood&&lowGood <= java.util.GregorianCalendar.MAX_VALUES[1]+1;

computeNewHour

public int computeNewHour(int field,
                          int amount,
                          Date start,
                          int oldHour)

This should return the value by which oldHour changes once amount is added to it. It is done in this way to avoid the problem with rolling the hour over the onset or cease of daylight savings time.

Returns:

the value by which oldHour changes after amount is added

Specifications: pure

public normal_behavior
old int newHour = (int)((oldHour+amount)%(this.getMaximum(field)+1));
assignable \nothing;
ensures \result == newHour&&this.getMinimum(10) <= newHour&&newHour <= this.getMaximum(10);

computeMonth

public int computeMonth(int amount)

This should compute the new month value after amount is added to it.

Returns:

the new month value after amount is added

Specifications: pure

public normal_behavior
old int mon = (int)(this.get(2)+amount)%12;
assignable \nothing;
ensures \result == mon&&this.getMinimum(2) <= mon&&mon <= this.getMaximum(2);

computeWoy

public int computeWoy(int amount)

This should compute the new week of year value after amount is added to it. The rolling of this value depends on how many days per week, as this value can be changed. Steps should be taken to make sure the function rolls correctly to account for all of the aspects of the calendar.

Returns:

the new week of year value after amount is added

Specifications: pure

public normal_behavior
old int woy = this.get(3);
assignable \nothing;
ensures \result == woy&&1 <= woy&&woy <= 52;

computeIsoYear

public int computeIsoYear()

This should return the ISO year depending on the conditions of WEEK_OF_YEAR and MONTH. These values, in turn, depend on the calendar restrictions on these values.

Returns:

the ISO year

Specifications: pure

public normal_behavior
old int isoYear = this.get(1);
assignable \nothing;
ensures \result == isoYear&&this.getMinimum(1) <= isoYear&&isoYear <= this.getMaximum(1);

computeDayOfMonth

public int computeDayOfMonth(int amount)

This should compute the new day of week after amount is added to it. The day of week holds the value of the current day in the week (Sunday, Monday, etc.). This is changed when rolling occurs.

Returns:

the day of week after amount is added

Specifications: pure

public normal_behavior
old int day_of_month = 0;
assignable \nothing;
ensures \result == day_of_month&&this.getMinimum(5) <= day_of_month&&day_of_month <= this.getMaximum(5);

computeMin2

public long computeMin2()

This should compute min2 value used for computing the roll amount for DAY_OF_WEEK. Min2 is the number of days before the current day in the week in question.

Returns:

min2 for use in computing the DAY_OF_WEEK roll amount

Specifications: pure

public normal_behavior
old int leadDays = (int)(this.get(7)-this.getFirstDayOfWeek());
old long min2 = 0;
ensures \result == min2&&min2 == this.time-leadDays*java.util.GregorianCalendar.ONE_DAY;

computeValue

public int computeValue(int field,
                        int amount)

This should compute the new value for which to roll field after amount is added to it. This is computed for the standard roll instructions used for the default field.

Returns:

the new value for which to roll field after amount is added

Specifications: pure

public normal_behavior
old int fieldAmount = this.get(field);
old int value = 0;
assignable \nothing;
ensures \result == value&&this.getMinimum(field) <= fieldAmount+value&&fieldAmount+value < +this.getMaximum(field);

computeMillisInDay

public long computeMillisInDay(long millis)

This should return the number of milliseconds past midnight for for the date specified by millis. This should take into account the correct time zone.

Returns:

the number of milliseconds past midnight for the given date

Specifications: pure

public normal_behavior
ensures 0 <= \result &&\result < java.util.GregorianCalendar.ONE_DAY;

getOffsetsForComputeFields

public int[] getOffsetsForComputeFields()

This should return the number of milliseconds past midnight for for the date specified by millis. This should take into account the correct time zone.

Returns:

the number of milliseconds past midnight for the given date

Specifications: pure

public normal_behavior
ensures -java.util.GregorianCalendar.ONE_DAY <= \result [0]&&\result [0] <= java.util.GregorianCalendar.ONE_DAY&&-java.util.GregorianCalendar.ONE_DAY <= \result [1]&&\result [1] <= java.util.GregorianCalendar.ONE_DAY;

timeToFieldsVarsAreSet

public boolean timeToFieldsVarsAreSet()

This should return true if the isSet[field] methods all are true and if calendarFieldsAreSet() also returns true.

Returns:

true if all isSet[field] return true and if calendarFieldsAreSet(); false otherwise.

Specifications: pure

public normal_behavior
ensures this.isSet[0]&&this.isSet[1]&&this.isSet[2]&&this.isSet[5]&&this.isSet[7]&&this.isSet[6]&&this.isSet[3]&&this.isSet[4]&&this.isSet[8]&&this.calendarFieldsAreSet();

computeMillis

public long computeMillis()

Model methods used for computeTime() This should compute the number of milliseconds from the current values of the fields without DST or time zone adjustments

Returns:

the number of milliseconds from current values of the fields without DST or time zone adjustments.

Specifications: pure

public normal_behavior
old long millis = 0;
assignable \nothing;
ensures \result == millis&&0 <= millis;

computeZoneOffset

public int computeZoneOffset(long millis)

This should return the correct time zone offset for the current time zone and the given time, specified by the argument millis. This must work in all circumstances, no matter what the internal data structures contain.

Returns:

the number of milliseconds for the time zone offset from GMT

Specifications: pure

public normal_behavior
ensures -java.util.GregorianCalendar.ONE_DAY <= \result &&\result <= java.util.GregorianCalendar.ONE_DAY;

setGregorianChange

public void setGregorianChange(Date date)

Specifications:

public normal_behavior
old long cutoverDay = floorDivide(this.gregorianCutover,java.util.GregorianCalendar.ONE_DAY);
old java.util.GregorianCalendar cal = new java.util.GregorianCalendar(this.getTimeZone());

{|

requires date != null;
assignable gregorianCutover;
ensures this.gregorianCutover == date.getTime();

also

requires cutoverDay < 0&&this.normalizedGregorianCutover > 0;
assignable normalizedGregorianCutover, gregorianCutoverYear;
ensures this.normalizedGregorianCutover == (cutoverDay+1)*java.util.GregorianCalendar.ONE_DAY;

also

requires cutoverDay >= 0||this.normalizedGregorianCutover <= 0;
assignable normalizedGregorianCutover, gregorianCutoverYear;
ensures this.normalizedGregorianCutover == cutoverDay*java.util.GregorianCalendar.ONE_DAY;

also

requires cal.get(0) == 0;
assignable normalizedGregorianCutover, gregorianCutoverYear;
ensures this.gregorianCutoverYear == 1-\old(this.gregorianCutoverYear);

also

requires cal.get(0) != 0;
assignable normalizedGregorianCutover, gregorianCutoverYear;
ensures this.gregorianCutoverYear == cal.get(1);

|}

getGregorianChange

public final Date getGregorianChange()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result .getTime() == this.gregorianCutover;

isLeapYear

public boolean isLeapYear(int year)

Specifications: pure

public normal_behavior
requires year >= this.gregorianCutoverYear;
assignable \nothing;
ensures \result == ((year%4 == 0)&&((year%100 != 0)||(year%400 == 0)));

     also

public normal_behavior
requires year < this.gregorianCutoverYear;
assignable \nothing;
ensures \result == (year%4 == 0);

equals

public boolean equals(nullable Object obj)

Overrides:

equals in class Calendar

Specifications: (inherited)pure

     also

public normal_behavior
old java.util.GregorianCalendar gcal = (java.util.GregorianCalendar)obj;
requires obj != null;
assignable \nothing;
ensures obj instanceof java.util.GregorianCalendar&&this.gregorianCutover == gcal.gregorianCutover;

Specifications inherited from overridden method equals(Object obj) in class Calendar:
       pure

     also

public normal_behavior
old java.util.Calendar calendar = (java.util.Calendar)obj;
requires obj != null;
assignable \nothing;
ensures obj instanceof java.util.Calendar&&this.getTimeInMillis() == calendar.getTimeInMillis()&&this.lenient == calendar.lenient&&this.firstDayOfWeek == calendar.firstDayOfWeek&&this.minimalDaysInFirstWeek == calendar.minimalDaysInFirstWeek&&this.zone.equals(calendar.zone);

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 ;

hashCode

public int hashCode()

Overrides:

hashCode in class Calendar

Specifications inherited from overridden method in class Calendar:
      --- None ---

Specifications inherited from overridden method in class Object:

public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);

     also

public code normal_behavior
assignable \nothing;

add

public void add(int field,
                int amount)

Specifications:

     also

public normal_behavior
requires amount == 0;
assignable \nothing;

     also

public normal_behavior
old int year = this.get(1);

{|

ensures this.isComplete();

also

{|

requires field == 1;
assignable_redundantly fields[1], fields[0], isTimeSet, areFieldsSet, isSet[*];
ensures this.pinDayOfMonthIsSet(\old(this.fields[5]),this.fields[5]);
ensures_redundantly this.isSet[1]&&this.isSet[0]&&this.calendarFieldsAreSet();

also

requires year > 0;
assignable_redundantly fields[1], isTimeSet, areFieldsSet, isSet[1];
ensures_redundantly this.fields[1] == \old(this.fields[1])+amount&&this.isSet[1]&&this.calendarFieldsAreSet();

also

{|

requires year <= 0;
assignable_redundantly fields[1], fields[0], isTimeSet, areFieldsSet, isSet[*];
ensures_redundantly this.fields[1] == 1-\old(this.fields[1])&&this.isSet[1]&&this.isSet[0]&&this.calendarFieldsAreSet();

also

requires this.internalGetEra() == 1;
assignable_redundantly fields[0], isTimeSet, areFieldsSet, isSet[0];
ensures_redundantly this.fields[0] == 0&&this.isSet[0]&&this.calendarFieldsAreSet();

also

requires this.internalGetEra() == 0;
assignable_redundantly fields[0], isTimeSet, areFieldsSet, isSet[0];
ensures_redundantly this.fields[0] == 1&&this.isSet[0]&&this.calendarFieldsAreSet();

|}

|}

also

old int month = (int)(this.get(2)+amount);

{|

requires field == 2;
assignable_redundantly fields[1], fields[0], fields[2], isTimeSet, areFieldsSet, isSet[*];
ensures this.pinDayOfMonthIsSet(\old(this.fields[5]),this.fields[5]);
ensures_redundantly this.isSet[1]&&this.isSet[0]&&this.isSet[2]&&this.calendarFieldsAreSet();

also

{|

requires this.isYAmountNotZero((int)(this.get(2)+amount));

also

requires year > 0;
assignable_redundantly fields[1], isTimeSet, areFieldsSet, isSet[1];
ensures_redundantly this.fields[1] == \old(this.fields[1])+amount&&this.isSet[1]&&this.calendarFieldsAreSet();

also

{|

requires year <= 0;
assignable_redundantly fields[1], fields[0], isTimeSet, areFieldsSet, isSet[*];
ensures_redundantly this.fields[1] == 1-\old(this.fields[1])&&this.isSet[1]&&this.isSet[0]&&this.calendarFieldsAreSet();

also

requires this.internalGetEra() == 1;
assignable_redundantly fields[0], isTimeSet, areFieldsSet, isSet[0];
ensures_redundantly this.fields[0] == 0&&this.isSet[0]&&this.calendarFieldsAreSet();

also

requires this.internalGetEra() == 0;
assignable_redundantly fields[0], isTimeSet, areFieldsSet, isSet[0];
ensures_redundantly this.fields[0] == 1&&this.isSet[0]&&this.calendarFieldsAreSet();

|}

also

requires month >= 0;
assignable_redundantly fields[2], isTimeSet, areFieldsSet, isSet[2];
ensures_redundantly this.fields[2] == (int)(month%12)&&this.isSet[2]&&this.calendarFieldsAreSet();

also

requires month < 0;
assignable_redundantly fields[2], isTimeSet, areFieldsSet, isSet[2];
ensures_redundantly this.fields[2] == 0+month&&this.isSet[2]&&this.calendarFieldsAreSet();

|}

|}

also

old int era = this.get(0);
requires field == 0;
assignable_redundantly fields[0], isTimeSet, areFieldsSet, isSet[0];
ensures_redundantly this.fields[0] == era&&this.isSet[0]&&this.calendarFieldsAreSet();

also

requires field == 3||field == 4||field == 8||field == 9||field == 5||field == 6||field == 7||field == 11||field == 10||field == 12||field == 13||field == 14;
assignable \nothing;

also

{|

assignable_redundantly time, isTimeSet, areFieldsSet, areAllFieldsSet, System.clock;
ensures this.getTimeInMillis() == this.time+this.computeDelta(field,amount);
ensures_redundantly this.milliFieldsAreSet();

also

old boolean adjustDST = (field == 3||field == 4||field == 8||field == 9||field == 5||field == 6||field == 7);
old int oldDSTOffset = this.get(16);
requires adjustDST&&this.computeDST(adjustDST,oldDSTOffset,this.get(16)) != 0;
assignable_redundantly time, isTimeSet, areFieldsSet, areAllFieldsSet, System.clock;
ensures this.getTimeInMillis() == this.time+this.computeDST(adjustDST,oldDSTOffset,this.get(16));
ensures_redundantly this.milliFieldsAreSet();

|}

|}

     also

public exceptional_behavior
requires field != 3||field != 4||field != 8||field != 9||field != 5||field != 6||field != 7||field != 11||field != 10||field != 12||field != 13||field != 14;
assignable \nothing;
signals_only java.lang.IllegalArgumentException;

Specifications inherited from overridden method add(int field, int amount) in class Calendar:

public normal_behavior
assignable fields[*];
ensures (* fields[field] has been increased by amount and all appropriate corresponding fields have been updated *);

roll

public void roll(int fld,
                 boolean up)

Specifications:

     also

public normal_behavior
requires up;
assignable fields[*];

     also

public normal_behavior
requires !up;
assignable fields[*];

     also

public model_program { ... }

Specifications inherited from overridden method roll(int field, boolean up) in class Calendar:

public normal_behavior
requires up;
assignable fields[*];
ensures (* fields[field] has been increased by one based on its restraints without changing larger fields *);

     also

public normal_behavior
requires !up;
assignable fields[*];
ensures (* fields[field] has been decreased by one based on its restraints without changing larger fields *);

roll

public void roll(int field,
                 int amount)

Overrides:

roll in class Calendar

Specifications:

     also

public normal_behavior
requires amount == 0;
assignable \nothing;

     also

public normal_behavior
requires field == 0||field == 1||field == 9||field == 12||field == 13||field == 14||field == 5;
assignable \nothing;
ensures this.isComplete();

     also

public normal_behavior
old java.util.Date start = this.getTime();
old int oldHour = this.get(field);
old int newHour = this.computeNewHour(field,amount,start,oldHour);
requires field == 10||field == 11;
assignable time, isTimeSet, areFieldsSet, areAllFieldsSet, System.clock;
ensures this.getTimeInMillis() == start.getTime()+java.util.GregorianCalendar.ONE_HOUR*(newHour-oldHour);
ensures_redundantly this.milliFieldsAreSet();

     also

public normal_behavior
old int mon = this.computeMonth(amount);
old int monthLen = this.monthLength(mon);
old int dom = this.get(5);

{|

requires field == 2;
assignable fields[2], fields[5], isTimeSet, areFieldsSet, isSet[*];
ensures this.fields[2] == mon&&this.isSet[2]&&this.isSet[5]&&this.calendarFieldsAreSet();

also

requires dom > monthLen;
assignable fields[5], isTimeSet, areFieldsSet, isSet[5];
ensures this.fields[5] == monthLen&&this.isSet[5]&&this.calendarFieldsAreSet();

|}

     also

public normal_behavior
old int woy = this.computeWoy(amount);
old int isoYear = this.computeIsoYear();
requires field == 3;
assignable fields[3], fields[1], isTimeSet, areFieldsSet, isSet[*];
ensures this.fields[3] == woy&&this.fields[1] == isoYear&&this.isSet[3]&&this.isSet[1]&&this.calendarFieldsAreSet();

     also

public normal_behavior
old int day_of_month = this.computeDayOfMonth(amount);
requires field == 4;
assignable fields[5], isTimeSet, areFieldsSet, isSet[5];
ensures this.fields[5] == day_of_month&&this.isSet[5]&&this.calendarFieldsAreSet();

     also

public normal_behavior
old long oldTime = this.time;
old long delta = (long)(amount*java.util.GregorianCalendar.ONE_DAY);
old long min2 = (long)(oldTime-(this.get(6)-1)*java.util.GregorianCalendar.ONE_DAY);
old int yearLength = this.yearLength();

{|

requires field == 6;
assignable time, isTimeSet, areFieldsSet, areAllFieldsSet, System.clock;
ensures this.getTimeInMillis() <= this.time+min2;
ensures_redundantly this.milliFieldsAreSet();

also

{|

requires oldTime >= 0;
assignable time;
ensures this.time == (oldTime+delta-min2)%(yearLength*java.util.GregorianCalendar.ONE_DAY);

also

requires oldTime < 0;
assignable time;
ensures this.time == ((oldTime+delta-min2)%(yearLength*java.util.GregorianCalendar.ONE_DAY))+yearLength*java.util.GregorianCalendar.ONE_DAY;

|}

|}

     also

public normal_behavior
old long min2 = this.computeMin2();
old long delta = (long)(amount*java.util.GregorianCalendar.ONE_DAY);

{|

requires field == 7;
assignable time, isTimeSet, areFieldsSet, areAllFieldsSet, System.clock;
ensures this.getTimeInMillis() == this.time+min2;
ensures_redundantly this.milliFieldsAreSet();

also

requires this.time >= 0;
assignable time;
ensures this.time == (this.time+delta-min2)%java.util.GregorianCalendar.ONE_WEEK;

also

requires this.time < 0;
assignable time;
ensures this.time == ((this.time+delta-min2)%java.util.GregorianCalendar.ONE_WEEK)+java.util.GregorianCalendar.ONE_WEEK;

|}

     also

public normal_behavior
old long oldTime = this.time;
old long delta = (long)(amount*java.util.GregorianCalendar.ONE_WEEK);
old int preWeeks = (int)((this.get(5)-1)/7);
old int postWeeks = (int)((this.monthLength(this.get(2))-this.get(5))/7);
old long min2 = (long)(oldTime-preWeeks*java.util.GregorianCalendar.ONE_WEEK);
old long gap2 = (long)(java.util.GregorianCalendar.ONE_WEEK*(preWeeks+postWeeks+1));

{|

requires field == 8;
assignable time, isTimeSet, areFieldsSet, areAllFieldsSet, System.clock;
ensures this.getTimeInMillis() <= this.time+min2;
ensures_redundantly this.milliFieldsAreSet();

also

{|

requires this.time >= 0;
assignable time;
ensures this.time == (oldTime+delta-min2)%gap2;

also

requires this.time < 0;
assignable time;
ensures this.time == ((oldTime+delta-min2)%gap2)+gap2;

|}

|}

     also

public exceptional_behavior
requires field != 0||field != 1||field != 9||field != 12||field != 13||field != 14||field != 5||field != 10||field != 11||field != 2||field != 3||field != 4||field != 6||field != 7||field != 8;
assignable \nothing;
signals_only java.lang.IllegalArgumentException;

     also

public normal_behavior
old int value = this.computeValue(field,amount);
assignable fields[field], isTimeSet, areFieldsSet, isSet[field];
ensures this.fields[field] == value&&this.isSet[field]&&this.calendarFieldsAreSet();

Specifications inherited from overridden method roll(int field, int amount) in class Calendar:

public normal_behavior
assignable fields[*];
ensures (* fields[field] has been incremented by amount based on its restraints without changing larger fields *);

getMinimum

public int getMinimum(int field)

Specifications: pure

     also

public normal_behavior
requires 0 <= field&&field <= java.util.GregorianCalendar.MIN_VALUES.length;
assignable \nothing;
ensures \result == java.util.GregorianCalendar.MIN_VALUES[field];

Specifications inherited from overridden method getMinimum(int field) in class Calendar:
       pure

public normal_behavior
requires 0 <= field&&field < 17;
assignable \nothing;
ensures this.resultIsMinimum();

getMaximum

public int getMaximum(int field)

Specifications: pure

     also

public normal_behavior
requires 0 <= field&&field <= java.util.GregorianCalendar.MAX_VALUES.length;
assignable \nothing;
ensures \result == java.util.GregorianCalendar.MAX_VALUES[field];

Specifications inherited from overridden method getMaximum(int field) in class Calendar:
       pure

public normal_behavior
requires 0 <= field&&field < 17;
assignable \nothing;
ensures this.resultIsMaximum();

getGreatestMinimum

public int getGreatestMinimum(int field)

Specifications: pure

     also

public normal_behavior
requires 0 <= field&&field <= java.util.GregorianCalendar.MIN_VALUES.length;
assignable \nothing;
ensures \result == java.util.GregorianCalendar.MIN_VALUES[field];

Specifications inherited from overridden method getGreatestMinimum(int field) in class Calendar:
       pure

public normal_behavior
requires 0 <= field&&field < 17;
assignable \nothing;
ensures this.resultIsMinimum();

getLeastMaximum

public int getLeastMaximum(int field)

Specifications: pure

     also

public normal_behavior
requires 0 <= field&&field <= java.util.GregorianCalendar.LEAST_MAX_VALUES.length;
assignable \nothing;
ensures \result == java.util.GregorianCalendar.LEAST_MAX_VALUES[field];

Specifications inherited from overridden method getLeastMaximum(int field) in class Calendar:
       pure

public normal_behavior
requires 0 <= field&&field < 17;
assignable \nothing;
ensures this.resultIsMaximum();

getActualMinimum

public int getActualMinimum(int field)

Overrides:

getActualMinimum in class Calendar

Specifications: pure

     also

public normal_behavior
requires 0 <= field&&field <= java.util.GregorianCalendar.MIN_VALUES.length;
assignable \nothing;
ensures \result == java.util.GregorianCalendar.MIN_VALUES[field];

Specifications inherited from overridden method getActualMinimum(int field) in class Calendar:
       pure

public normal_behavior
requires 0 <= field&&field < 17;
assignable \nothing;
ensures this.resultIsMinimum();

getActualMaximum

public int getActualMaximum(int field)

Overrides:

getActualMaximum in class Calendar

Specifications: pure

     also

public normal_behavior
requires field == 5;
assignable \nothing;
ensures \result == this.monthLength(this.get(2));

     also

public normal_behavior
requires field == 6;
assignable \nothing;
ensures \result == this.yearLength();

     also

public normal_behavior
requires field == 3||field == 4||field == 8;
assignable \nothing;
ensures \result == super.getActualMaximum(field);

     also

public normal_behavior
requires field == 1;
assignable \nothing;
ensures \result == this.computeLowGood();

     also

public normal_behavior
requires field != 5&&field != 6&&field != 3&&field != 4&&field != 8&&field != 1;
assignable \nothing;
ensures \result == this.getMaximum(field);

Specifications inherited from overridden method getActualMaximum(int field) in class Calendar:
       pure

public normal_behavior
requires 0 <= field&&field < 17;
assignable \nothing;
ensures this.resultIsMaximum();

inDaylightTime

boolean inDaylightTime()

Specifications:

normal_behavior
requires !this.getTimeZone().useDaylightTime();
assignable \nothing;
ensures \result == false;

     also

normal_behavior
requires this.getTimeZone().useDaylightTime();
assignable \nothing;
ensures \result == (this.get(16) != 0);
ensures_redundantly this.isComplete();

getISOYear

int getISOYear()

Specifications: pure

normal_behavior
old int isoYear = this.get(1);
assignable \nothing;
ensures \result == isoYear;
ensures_redundantly this.isComplete();

computeFields

protected void computeFields()

Specifications:

     also

protected normal_behavior
old long valueForMillis = this.computeMillisInDay(this.time);
old long valueForSecond = (long)(valueForMillis/1000);
old long valueForMinute = (long)(valueForSecond/60);
old int[] offsets = this.getOffsetsForComputeFields();
assignable fields[14], fields[13], fields[12], fields[11], fields[9], fields[10], fields[15], fields[16], isTimeSet, areFieldsSet, isSet[*];
ensures this.timeToFieldsVarsAreSet()&&this.fields[14] == valueForMillis%1000&&this.fields[13] == valueForSecond%60&&this.fields[12] == valueForMinute%60&&this.fields[11] == valueForMillis&&this.fields[9] == valueForMillis/12&&this.fields[10] == valueForMillis%12&&this.fields[15] == offsets[0]&&this.fields[16] == offsets[1]&&( \forall int i; 0 <= i&&i < 17; this.stamp[i] == java.util.Calendar.INTERNALLY_SET&&this.isSet[i])&&this.isSet[14]&&this.isSet[13]&&this.isSet[12]&&this.isSet[11]&&this.isSet[9]&&this.isSet[10]&&this.isSet[15]&&this.isSet[16]&&this.calendarFieldsAreSet();

Specifications inherited from overridden method in class Calendar:

protected normal_behavior
assignable fields[*];
ensures this.correspondsTimeAndFields();

computeTime

protected void computeTime()

Specifications:

     also

protected exceptional_behavior
requires !this.isLenient()&&!this.validateFields();
assignable \nothing;
signals_only java.lang.IllegalArgumentException;

     also

protected exceptional_behavior
requires this.get(0) != 0||this.get(0) != 1;
assignable \nothing;
signals_only java.lang.IllegalArgumentException;

     also

protected normal_behavior
old long millis = this.computeMillis();
old int zoneOffset = this.computeZoneOffset(millis);

{|

requires this.stamp[16] < java.util.Calendar.MINIMUM_USER_STAMP;
assignable time;
ensures this.time == millis-zoneOffset;

also

requires this.stamp[16] >= java.util.Calendar.MINIMUM_USER_STAMP;
assignable time;
ensures this.time == millis-zoneOffset-this.get(16);

|}

Specifications inherited from overridden method in class Calendar:

protected normal_behavior
assignable time;
ensures this.correspondsTimeAndFields();

floorDivide

private static final long floorDivide(long numerator,
                                      long denominator)

Specifications: pure spec_public

private normal_behavior
requires numerator >= 0;
assignable \nothing;
ensures \result == numerator/denominator;

     also

private normal_behavior
requires numerator < 0;
assignable \nothing;
ensures \result == ((numerator+1)/denominator)-1;

monthLength

private final int monthLength(int month)

Specifications: pure spec_public

private normal_behavior
old int year = this.internalGet(1);

{|

requires this.isLeapYear(year);
assignable \nothing;
ensures \result == java.util.GregorianCalendar.LEAP_MONTH_LENGTH[month];

also

requires !this.isLeapYear(year);
assignable \nothing;
ensures \result == java.util.GregorianCalendar.MONTH_LENGTH[month];

|}

validateFields

private boolean validateFields()

Specifications: pure spec_public

private normal_behavior
requires ( \forall int field; 0 <= field&&field < 17; field != 5&&field != 6&&this.isSet(field)&&!this.boundsCheck(this.internalGet(field),field));
assignable \nothing;
ensures \result == false;

     also

private normal_behavior
requires ( \forall int field; 0 <= field&&field < 17; field == 5||field == 6||!this.isSet(field)||this.boundsCheck(this.internalGet(field),field));
assignable \nothing;
ensures \result == true;

     also

private normal_behavior
requires this.stamp[5] >= java.util.Calendar.MINIMUM_USER_STAMP&&(this.get(5) < this.getMinimum(5)||this.get(5) > this.monthLength(this.get(2)));
assignable \nothing;
ensures \result == false;

     also

private normal_behavior
requires this.stamp[5] < java.util.Calendar.MINIMUM_USER_STAMP||(this.get(5) >= this.getMinimum(5)&&this.get(5) <= this.monthLength(this.get(2)));
assignable \nothing;
ensures \result == true;

     also

private normal_behavior
requires this.stamp[6] >= java.util.Calendar.MINIMUM_USER_STAMP&&(this.get(6) < 1||this.get(6) > this.yearLength());
assignable \nothing;
ensures \result == false;

     also

private normal_behavior
requires this.stamp[6] < java.util.Calendar.MINIMUM_USER_STAMP||(this.get(6) >= 1&&this.get(6) <= this.yearLength());
assignable \nothing;
ensures \result == true;

     also

private normal_behavior
requires this.isSet(8)&&0 == this.internalGet(8);
assignable \nothing;
ensures \result == false;

     also

private normal_behavior
requires !this.isSet(8)||0 != this.internalGet(8);
assignable \nothing;
ensures \result == true;

boundsCheck

private final boolean boundsCheck(int value,
                                  int field)

Specifications: pure spec_public

private normal_behavior
assignable \nothing;
ensures \result == (this.getMinimum(field) <= value&&value <= this.getMaximum(field));

internalGetEra

private final int internalGetEra()

Specifications: pure spec_public

private normal_behavior
requires this.isSet(0);
assignable \nothing;
ensures \result == this.internalGet(0);

     also

private normal_behavior
requires !this.isSet(0);
assignable \nothing;
ensures \result == 1;

yearLength

private final int yearLength()

Specifications: pure spec_public

private normal_behavior
requires this.isLeapYear(this.get(1));
assignable \nothing;
ensures \result == 366;

     also

private normal_behavior
requires !this.isLeapYear(this.get(1));
assignable \nothing;
ensures \result == 365;