java.util
Class Date
java.lang.Object
java.util.Date
- All Implemented Interfaces:
- Cloneable, Comparable, Serializable
- Direct Known Subclasses:
- Date, Time, Timestamp
- public class Date
- extends Object
- implements Serializable, Cloneable, Comparable
JML's specification of java.util.Date.
Some of this specification is taken from ESC/Java.
- Version:
- $Revision: 1.14 $
- Author:
- Kristina Boysen
| Specifications inherited from class Object |
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this); |
| Specifications inherited from interface Comparable |
instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0);
instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x)));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z))); |
|
Constructor Summary |
Date()
|
Date(int year,
int month,
int date)
Deprecated. as of JDK 1.1 |
Date(int year,
int month,
int date,
int hrs,
int min)
Deprecated. as of JDK 1.1 |
Date(int year,
int month,
int date,
int hrs,
int min,
int sec)
Deprecated. as of JDK 1.1 |
Date(String s)
Deprecated. as of JDK 1.1 |
Date(long date)
|
cal
private transient Calendar cal
- Specifications: spec_public
fastTime
private transient long fastTime
- Specifications: spec_public
Date
public Date()
- Specifications:
-
public normal_behavior
assignable fastTime, System.clock;
ensures this.cal == null;
Date
public Date(long date)
- Specifications:
-
public normal_behavior
assignable fastTime;
ensures this.cal == null&&this.fastTime == date;
Date
public Date(int year,
int month,
int date)
- Deprecated. as of JDK 1.1
Date
public Date(int year,
int month,
int date,
int hrs,
int min)
- Deprecated. as of JDK 1.1
Date
public Date(int year,
int month,
int date,
int hrs,
int min,
int sec)
- Deprecated. as of JDK 1.1
Date
public Date(String s)
- Deprecated. as of JDK 1.1
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]);
UTC
public static long UTC(int year,
int month,
int date,
int hrs,
int min,
int sec)
- Deprecated. as of JDK 1.1
parse
public static long parse(String s)
- Deprecated. as of JDK 1.1
getYear
public int getYear()
- Deprecated. as of JDK 1.1
setYear
public void setYear(int year)
- Deprecated. as of JDK 1.1
getMonth
public int getMonth()
- Deprecated. as of JDK 1.1
setMonth
public void setMonth(int month)
- Deprecated. as of JDK 1.1
getDate
public int getDate()
- Deprecated. as of JDK 1.1
setDate
public void setDate(int date)
- Deprecated. as of JDK 1.1
getDay
public int getDay()
- Deprecated. as of JDK 1.1
getHours
public int getHours()
- Deprecated. as of JDK 1.1
setHours
public void setHours(int hours)
- Deprecated. as of JDK 1.1
getMinutes
public int getMinutes()
- Deprecated. as of JDK 1.1
setMinutes
public void setMinutes(int minutes)
- Deprecated. as of JDK 1.1
getSeconds
public int getSeconds()
- Deprecated. as of JDK 1.1
setSeconds
public void setSeconds(int seconds)
- Deprecated. as of JDK 1.1
getTime
public long getTime()
- Specifications: pure
-
public normal_behavior
requires this.cal == null;
assignable \nothing;
ensures \result == this.fastTime;
- also
-
public normal_behavior
requires this.cal != null;
assignable \nothing;
ensures \result == this.cal.getTimeInMillis();
setTime
public void setTime(long time)
- Specifications:
-
public normal_behavior
requires this.cal == null;
assignable fastTime;
ensures this.fastTime == time;
- also
-
public normal_behavior
requires this.cal != null;
assignable cal;
ensures time == this.cal.getTimeInMillis();
before
public boolean before(Date when)
- Specifications: pure
-
public normal_behavior
requires when != null&&this.getTime() < when.getTime();
assignable \nothing;
ensures \result == true;
- also
-
public normal_behavior
requires when != null&&this.getTime() >= when.getTime();
ensures \result == false;
after
public boolean after(Date when)
- Specifications: pure
-
public normal_behavior
requires when != null&&this.getTime() > when.getTime();
assignable \nothing;
ensures \result == true;
- also
-
public normal_behavior
requires when != null&&this.getTime() <= when.getTime();
ensures \result == false;
equals
public boolean equals(nullable Object obj)
- Overrides:
equals in class Object
- Specifications: pure
- also
-
public normal_behavior
old java.util.Date date = (java.util.Date)obj;
requires obj != null;
assignable \nothing;
ensures \result ==> (obj instanceof java.util.Date&&this.getTime() == date.getTime());
- 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 ;
compareTo
public int compareTo(non_null Date anotherDate)
- Specifications: pure
-
public normal_behavior
requires anotherDate != null&&this.before(anotherDate);
assignable \nothing;
ensures \result < 0;
- also
-
public normal_behavior
requires anotherDate != null&&this.equals(anotherDate);
assignable \nothing;
ensures \result == 0;
- also
-
public normal_behavior
requires anotherDate != null&&this.after(anotherDate);
assignable \nothing;
ensures \result > 0;
- Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
pure -
public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
- also
-
public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);
compareTo
public int compareTo(non_null Object o)
- Specified by:
compareTo in interface Comparable
- Specifications: pure
- also
-
public normal_behavior
requires o != null&&o instanceof java.util.Date;
assignable \nothing;
ensures \result == this.compareTo((java.util.Date)o);
- Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
pure -
public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
- also
-
public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);
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;
toString
public String toString()
- Overrides:
toString in class Object
- Specifications:
- also
-
public normal_behavior
assignable \nothing;
ensures (* \result is the String representation of Date *);
- 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;
toLocaleString
public String toLocaleString()
- Deprecated. as of JDK 1.1
toGMTString
public String toGMTString()
- Deprecated. as of JDK 1.1
getTimezoneOffset
public int getTimezoneOffset()
- Deprecated. as of JDK 1.1
JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.