java.util
Class Calendar

java.lang.Object
  java.util.Calendar

All Implemented Interfaces:

Cloneable, Serializable

Direct Known Subclasses:

GregorianCalendar

public abstract class Calendar

extends Object

implements Serializable, Cloneable

JML's specification of java.util.Calendar. Some of this specification is taken from ESC/Java.

Version:

$Revision: 1.17 $

Author:

Kristina Boysen, Gary T. Leavens

Class Specifications

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
Locale	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	AM
static int	AM_PM
static int	APRIL
[spec_public] (package private)  boolean	areAllFieldsSet
[spec_public] protected  boolean	areFieldsSet
static int	AUGUST
[spec_public] private static Hashtable	cachedLocaleData
(package private) static int	currentSerialVersion
static int	DATE
static int	DAY_OF_MONTH
static int	DAY_OF_WEEK
static int	DAY_OF_WEEK_IN_MONTH
static int	DAY_OF_YEAR
static int	DECEMBER
static int	DST_OFFSET
static int	ERA
static int	FEBRUARY
static int	FIELD_COUNT
[spec_public] protected  int[]	fields
[spec_public] private  int	firstDayOfWeek
static int	FRIDAY
static int	HOUR
static int	HOUR_OF_DAY
[spec_public] (package private) static int	INTERNALLY_SET
[spec_public] protected  boolean[]	isSet
[spec_public] protected  boolean	isTimeSet
static int	JANUARY
static int	JULY
static int	JUNE
[spec_public] private  boolean	lenient
static int	MARCH
static int	MAY
static int	MILLISECOND
[spec_public] private  int	minimalDaysInFirstWeek
[spec_public] (package private) static int	MINIMUM_USER_STAMP
static int	MINUTE
static int	MONDAY
static int	MONTH
static int	NOVEMBER
static int	OCTOBER
static int	PM
static int	SATURDAY
static int	SECOND
static int	SEPTEMBER
(package private) static long	serialVersionUID
[spec_public] (package private)  int[]	stamp
static int	SUNDAY
static int	THURSDAY
[spec_public] protected  long	time
static int	TUESDAY
static int	UNDECIMBER
[spec_public] (package private) static int	UNSET
static int	WEDNESDAY
static int	WEEK_OF_MONTH
static int	WEEK_OF_YEAR
static int	YEAR
[spec_public] private  TimeZone	zone
static int	ZONE_OFFSET

 

Constructor Summary
protected	Calendar()
protected	Calendar(TimeZone zone, Locale aLocale)           firstDayOfWeek and minimalDaysInFirstWeek are both set in private void setWeekCountData(Locale desiredLocale), which I did not write specifications for since it is private.

 

Model Method Summary
boolean	correspondsTimeAndFields()           For use with computeTime() and computeFields(), which are dual methods.
boolean	resultIsMaximum()           For use with getMaximum(), getGreatestMaximum(), and getActualMaximum(), since these all ensure basically the same thing.
boolean	resultIsMinimum()           For use with getMinimum(), getGreatestMinimum(), and getActualMinimum(), since these all ensure basically the same thing.

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
abstract  void	add(int field, int amount)
boolean	after(Object when)
boolean	before(Object when)
void	clear()
void	clear(int field)
Object	clone()
protected  void	complete()
protected abstract  void	computeFields()
protected abstract  void	computeTime()
boolean	equals(nullable Object obj)
int	get(int field)
int	getActualMaximum(int field)
int	getActualMinimum(int field)
static Locale[]	getAvailableLocales()
int	getFirstDayOfWeek()
abstract  int	getGreatestMinimum(int field)
static Calendar	getInstance()
static Calendar	getInstance(Locale aLocale)
static Calendar	getInstance(TimeZone zone)
static Calendar	getInstance(TimeZone zone, Locale aLocale)
abstract  int	getLeastMaximum(int field)
abstract  int	getMaximum(int field)
int	getMinimalDaysInFirstWeek()
abstract  int	getMinimum(int field)
Date	getTime()
long	getTimeInMillis()
TimeZone	getTimeZone()
int	hashCode()
protected  int	internalGet(int field)
(package private)  void	internalSet(int field, int value)
boolean	isLenient()
boolean	isSet(int field)
abstract  void	roll(int field, boolean up)
void	roll(int field, int amount)
void	set(int field, int value)
void	set(int year, int month, int date)
void	set(int year, int month, int date, int hour, int minute)
void	set(int year, int month, int date, int hour, int minute, int second)
void	setFirstDayOfWeek(int value)
void	setLenient(boolean lenient)
void	setMinimalDaysInFirstWeek(int value)
void	setTime(Date date)
void	setTimeInMillis(long millis)
void	setTimeZone(TimeZone value)
String	toString()

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

locale

public Locale locale

ERA

public static final int ERA

YEAR

public static final int YEAR

MONTH

public static final int MONTH

WEEK_OF_YEAR

public static final int WEEK_OF_YEAR

WEEK_OF_MONTH

public static final int WEEK_OF_MONTH

DATE

public static final int DATE

DAY_OF_MONTH

public static final int DAY_OF_MONTH

DAY_OF_YEAR

public static final int DAY_OF_YEAR

DAY_OF_WEEK

public static final int DAY_OF_WEEK

DAY_OF_WEEK_IN_MONTH

public static final int DAY_OF_WEEK_IN_MONTH

AM_PM

public static final int AM_PM

HOUR

public static final int HOUR

HOUR_OF_DAY

public static final int HOUR_OF_DAY

MINUTE

public static final int MINUTE

SECOND

public static final int SECOND

MILLISECOND

public static final int MILLISECOND

ZONE_OFFSET

public static final int ZONE_OFFSET

DST_OFFSET

public static final int DST_OFFSET

FIELD_COUNT

public static final int FIELD_COUNT

SUNDAY

public static final int SUNDAY

MONDAY

public static final int MONDAY

TUESDAY

public static final int TUESDAY

WEDNESDAY

public static final int WEDNESDAY

THURSDAY

public static final int THURSDAY

FRIDAY

public static final int FRIDAY

SATURDAY

public static final int SATURDAY

JANUARY

public static final int JANUARY

FEBRUARY

public static final int FEBRUARY

MARCH

public static final int MARCH

APRIL

public static final int APRIL

MAY

public static final int MAY

JUNE

public static final int JUNE

JULY

public static final int JULY

AUGUST

public static final int AUGUST

SEPTEMBER

public static final int SEPTEMBER

OCTOBER

public static final int OCTOBER

NOVEMBER

public static final int NOVEMBER

DECEMBER

public static final int DECEMBER

UNDECIMBER

public static final int UNDECIMBER

AM

public static final int AM

PM

public static final int PM

fields

protected int[] fields

Specifications: spec_public

isSet

protected boolean[] isSet

Specifications: spec_public

stamp

transient int[] stamp

Specifications: spec_public

time

protected long time

Specifications: spec_public

isTimeSet

protected boolean isTimeSet

Specifications: spec_public

areFieldsSet

protected boolean areFieldsSet

Specifications: spec_public

areAllFieldsSet

transient boolean areAllFieldsSet

Specifications: spec_public

lenient

private boolean lenient

Specifications: spec_public

zone

private TimeZone zone

Specifications: spec_public

firstDayOfWeek

private int firstDayOfWeek

Specifications: spec_public

minimalDaysInFirstWeek

private int minimalDaysInFirstWeek

Specifications: spec_public

cachedLocaleData

private static Hashtable cachedLocaleData

Specifications: spec_public

UNSET

static final int UNSET

Specifications: spec_public

INTERNALLY_SET

static final int INTERNALLY_SET

Specifications: spec_public

MINIMUM_USER_STAMP

static final int MINIMUM_USER_STAMP

Specifications: spec_public

currentSerialVersion

static final int currentSerialVersion

serialVersionUID

static final long serialVersionUID

Calendar

protected Calendar()

Specifications:

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

Calendar

protected Calendar(TimeZone zone,
                   Locale aLocale)

firstDayOfWeek and minimalDaysInFirstWeek are both set in private void setWeekCountData(Locale desiredLocale), which I did not write specifications for since it is private. The first line calls on the Hashtable cachedLocaleData, and this data is needed to check correct assignment to firstDayOfWeek and minimalDaysInFirstWeek.

Specifications:

protected normal_behavior
old int[] data = (int[])java.util.Calendar.cachedLocaleData.get(aLocale);
requires zone != null&&aLocale != null;
assignable this.zone, locale, firstDayOfWeek, minimalDaysInFirstWeek;
ensures this.zone.equals(zone)&&this.locale.equals(aLocale)&&this.firstDayOfWeek == data[0]&&this.minimalDaysInFirstWeek == data[1];

correspondsTimeAndFields

public boolean correspondsTimeAndFields()

For use with computeTime() and computeFields(), which are dual methods. Each method ensures that the boolean below is true.

Specifications: pure

public normal_behavior
ensures (* fields[*] is now a representation of time and vice versa *);

resultIsMinimum

public boolean resultIsMinimum()

For use with getMinimum(), getGreatestMinimum(), and getActualMinimum(), since these all ensure basically the same thing.

Specifications: pure

public normal_behavior
ensures (* \result is the minimum for this field *);

resultIsMaximum

public boolean resultIsMaximum()

For use with getMaximum(), getGreatestMaximum(), and getActualMaximum(), since these all ensure basically the same thing.

Specifications: pure

public normal_behavior
ensures (* \result is the maximum for this field *);

getInstance

public static Calendar getInstance()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result != null;

getInstance

public static Calendar getInstance(TimeZone zone)

Specifications: pure

public normal_behavior
requires zone != null;
assignable \nothing;
ensures \result != null&&\result .zone.equals(zone);

getInstance

public static Calendar getInstance(Locale aLocale)

Specifications: pure

public normal_behavior
requires aLocale != null;
assignable \nothing;
ensures \result != null&&\result .locale.equals(aLocale);

getInstance

public static Calendar getInstance(TimeZone zone,
                                   Locale aLocale)

Specifications: pure

public normal_behavior
requires zone != null&&aLocale != null;
assignable \nothing;
ensures \result != null&&\result .zone.equals(zone)&&\result .locale.equals(aLocale);

getAvailableLocales

public static Locale[] getAvailableLocales()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \nonnullelements(\result )&&\result .equals(java.text.DateFormat.getAvailableLocales());

computeTime

protected abstract void computeTime()

Specifications:

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

computeFields

protected abstract void computeFields()

Specifications:

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

getTime

public final Date getTime()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result != null&&\result .getTime() == this.getTimeInMillis();

setTime

public final void setTime(Date date)

Specifications:

public normal_behavior
requires date != null;
assignable \nothing;
ensures date.getTime() == this.getTimeInMillis();

getTimeInMillis

public long getTimeInMillis()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.time;

setTimeInMillis

public void setTimeInMillis(long millis)

Specifications:

public normal_behavior
assignable isTimeSet, areFieldsSet, areAllFieldsSet;
ensures this.time == millis&&this.isTimeSet&&this.areFieldsSet&&this.areAllFieldsSet;

get

public int get(int field)

Specifications: pure

public normal_behavior
requires 0 <= field&&field < 17;
assignable \nothing;
ensures \result == this.fields[field];

internalGet

protected final int internalGet(int field)

Specifications: pure

protected normal_behavior
requires_redundantly 0 <= field&&field < 17;
assignable \nothing;
ensures \result == this.fields[field];

internalSet

final void internalSet(int field,
                       int value)

Specifications:

normal_behavior
requires_redundantly 0 <= field&&field < 17;
assignable fields[field];
ensures this.fields[field] == value;

set

public void set(int field,
                int value)

Specifications:

public normal_behavior
requires 0 <= field&&field < 17;
assignable isTimeSet, areFieldsSet, stamp[*], isSet[*];
ensures !this.isTimeSet&&!this.areFieldsSet&&this.isSet[field];

set

public final void set(int year,
                      int month,
                      int date)

Specifications: pure

public normal_behavior
requires 0 <= year&&0 <= month&&1 <= date;
assignable \nothing;
ensures_redundantly this.fields[1] == year&&this.fields[2] == month&&this.fields[5] == date;

set

public final void set(int year,
                      int month,
                      int date,
                      int hour,
                      int minute)

Specifications: pure

public normal_behavior
requires 0 <= year&&0 <= month&&1 <= date&&0 <= hour&&0 <= minute;
assignable \nothing;
ensures_redundantly this.fields[1] == year&&this.fields[2] == month&&this.fields[5] == date&&this.fields[11] == hour&&this.fields[12] == minute;

set

public final void set(int year,
                      int month,
                      int date,
                      int hour,
                      int minute,
                      int second)

Specifications: pure

public normal_behavior
requires 0 <= year&&0 <= month&&1 <= date&&0 <= hour&&0 <= minute&&0 <= second;
assignable \nothing;
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;

clear

public final void clear()

Specifications:

public normal_behavior
assignable fields[*], stamp[*], areFieldsSet, areAllFieldsSet, isSet[*], isTimeSet;
ensures !this.areFieldsSet&&!this.areAllFieldsSet&&!this.isTimeSet&&this.fields != null&&this.stamp != null&&this.isSet != null;

clear

public final void clear(int field)

Specifications:

public normal_behavior
requires 0 <= field&&field < 17;
assignable fields[*], stamp[*], areFieldsSet, areAllFieldsSet, isSet[*], isTimeSet;
ensures this.fields[field] == 0&&this.stamp[field] == java.util.Calendar.UNSET&&!this.areFieldsSet&&!this.areAllFieldsSet&&!this.isSet[field]&&!this.isTimeSet;

isSet

public final boolean isSet(int field)

Specifications: pure

public normal_behavior
requires 0 <= field&&field < 17;
assignable \nothing;
ensures \result == (this.stamp[field] != java.util.Calendar.UNSET);

complete

protected void complete()

Specifications:

protected normal_behavior
assignable areFieldsSet, areAllFieldsSet;
ensures this.areFieldsSet&&this.areAllFieldsSet;

equals

public boolean equals(nullable Object obj)

Overrides:

equals in class Object

Specifications: 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 Object

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;

before

public boolean before(Object when)

Specifications: pure

public normal_behavior
requires when != null;
assignable \nothing;
ensures when instanceof java.util.Calendar&&\result == (this.getTimeInMillis() < ((java.util.Calendar)when).getTimeInMillis());

after

public boolean after(Object when)

Specifications: pure

public normal_behavior
requires when != null;
assignable \nothing;
ensures when instanceof java.util.Calendar&&\result == (this.getTimeInMillis() > ((java.util.Calendar)when).getTimeInMillis());

add

public abstract void add(int field,
                         int amount)

Specifications:

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

roll

public abstract void roll(int field,
                          boolean up)

Specifications:

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)

Specifications:

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

setTimeZone

public void setTimeZone(TimeZone value)

Specifications:

public normal_behavior
requires value != null;
assignable this.zone, areFieldsSet;
ensures this.zone.equals(value)&&!this.areFieldsSet;

getTimeZone

public TimeZone getTimeZone()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result .equals(this.zone);

setLenient

public void setLenient(boolean lenient)

Specifications:

public normal_behavior
assignable this.lenient;
ensures this.lenient == lenient;

isLenient

public boolean isLenient()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.lenient;

setFirstDayOfWeek

public void setFirstDayOfWeek(int value)

Specifications:

public normal_behavior
assignable firstDayOfWeek;
ensures this.firstDayOfWeek == value;

getFirstDayOfWeek

public int getFirstDayOfWeek()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.firstDayOfWeek;

setMinimalDaysInFirstWeek

public void setMinimalDaysInFirstWeek(int value)

Specifications:

public normal_behavior
assignable minimalDaysInFirstWeek;
ensures this.minimalDaysInFirstWeek == value;

getMinimalDaysInFirstWeek

public int getMinimalDaysInFirstWeek()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.minimalDaysInFirstWeek;

getMinimum

public abstract int getMinimum(int field)

Specifications: pure

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

getMaximum

public abstract int getMaximum(int field)

Specifications: pure

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

getGreatestMinimum

public abstract int getGreatestMinimum(int field)

Specifications: pure

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

getLeastMaximum

public abstract int getLeastMaximum(int field)

Specifications: pure

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

getActualMinimum

public int getActualMinimum(int field)

Specifications: pure

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

getActualMaximum

public int getActualMaximum(int field)

Specifications: pure

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

clone

public Object clone()

Overrides:

clone in class Object

Specifications:

     also

public normal_behavior
assignable \nothing;
ensures \fresh(\result )&&\result .equals(this);

Specifications inherited from overridden method in class Object:
       non_null

protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);

     also

protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));

     also

protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;

     also

protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);

toString

public String toString()

Overrides:

toString in class Object

Specifications: pure

     also

public normal_behavior
assignable \nothing;
ensures (* \result is the String representation of Calendar *);

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.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;