// @(#)$Id: Long.jml,v 1.22 2007/02/08 14:05:50 leavens Exp $ // Copyright (C) 2005 Iowa State University // // This file is part of the runtime library of the Java Modeling Language. // // This library is free software; you can redistribute it and/or // modify it under the terms of the GNU Lesser General Public License // as published by the Free Software Foundation; either version 2.1, // of the License, or (at your option) any later version. // // This library is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU // Lesser General Public License for more details. // // You should have received a copy of the GNU Lesser General Public License // along with JML; see the file LesserGPL.txt. If not, write to the Free // Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA // 02110-1301 USA. package java.lang; /** JML's specification of java.lang.Long. * @version $Revision: 1.22 $ * @author Brandon Shilling * @author Gary T. Leavens */ //-@ immutable public /*@ pure @*/ final class Long extends Number implements Comparable { //@ public model long theLong; /*@ @ public normal_behavior @ ensures \result == parseable( s, 10 ); @ model public static pure boolean parseable( String s ); @ public normal_behavior @ requires Character.MIN_RADIX <= r && r <= Character.MAX_RADIX; @ ensures \result <==> @ s != null && !s.equals("") && @ (\forall int i; 0 <= i && i < s.length(); @ Character.digit(s.charAt(i), r) != -1); @ also @ public normal_behavior @ requires Character.MIN_RADIX <= r && r <= Character.MAX_RADIX; @ ensures \result <==> @ s != null && !s.equals("") && @ (\forall int i; 1 <= i && i < s.length() @ && s.charAt(0) == '-'; @ Character.digit(s.charAt(i), r) != -1); @ model public static pure boolean parseable( String s, int r ); @ public normal_behavior @ requires nm.length() > 0; @ {| @ // positive hex @ requires (nm.length() >= 2 @ && nm.charAt(0) == 'O' && nm.charAt(1) == 'x'); @ ensures \result == parseable(nm.substring(2), 16); @ also @ // negative hex @ requires (nm.length() >= 3 @ && nm.charAt(0) == '-' && nm.charAt(1) == 'O' @ && nm.charAt(2) == 'x'); @ ensures \result == parseable(nm.substring(3), 16); @ also @ // positive hex @ requires (nm.charAt(0) == '#'); @ ensures \result == parseable(nm.substring(1), 16); @ also @ // negative hex @ requires (nm.length() >= 2 @ && nm.charAt(0) == '-' && nm.charAt(1) == '#'); @ ensures \result == parseable(nm.substring(2), 16); @ also @ // positive octal @ requires (nm.charAt(0) == 'O'); @ ensures \result == parseable(nm.substring(1), 8); @ also @ // negative octal @ requires (nm.length() >= 2 @ && nm.charAt(0) == '-' && nm.charAt(1) == 'O'); @ ensures \result == parseable(nm.substring(2), 8); @ also @ // positive or negative long, radix 10 @ requires !( (nm.length() >= 2 @ && nm.charAt(0) == 'O' && nm.charAt(1) == 'x') @ || (nm.length() >= 3 @ && nm.charAt(0) == '-' && nm.charAt(1) == 'O' @ && nm.charAt(2) == 'x') @ || (nm.charAt(0) == '#') @ || (nm.length() >= 2 @ && nm.charAt(0) == '-' && nm.charAt(1) == '#') @ || (nm.charAt(0) == 'O') @ || (nm.length() >= 2 @ && nm.charAt(0) == '-' && nm.charAt(1) == 'O') @ ); @ ensures \result == parseable(nm); @ |} @ model public static pure boolean decodeable( String nm ); @*/ public static final long MIN_VALUE; public static final long MAX_VALUE; /*@ public normal_behavior @ {| @ requires (Character.MIN_RADIX <= radix @ && radix <= Character.MAX_RADIX); @ {| @ requires i < 0; @ ensures \result != null && \result.length() >= 2 @ && \result.charAt(0) == '-' && \result.charAt(1) != '0' @ && i == parseLong(\result, radix); @ also @ requires i > 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(0) != '0' @ && i == parseLong(\result, radix); @ also @ requires i == 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(0) == '0' && \result.length() == 1; @ |} @ also @ requires (Character.MIN_RADIX > radix @ && radix > Character.MAX_RADIX); @ {| @ requires i < 0; @ ensures \result != null && \result.length() >= 2 @ && \result.charAt(0) == '-' && \result.charAt(1) != '0' @ && i == parseLong(\result, 10); @ also @ requires i > 0; @ ensures \result!= null && \result.length() >= 1 @ && \result.charAt(0) != '0' @ && i == parseLong(\result, 10); @ also @ requires i == 0; @ ensures \result != null && \result.length() == 1 @ && \result.charAt(0) == '0'; @ |} @ |} @ implies_that @ public normal_behavior @ ensures (* \result is a string representation of i @ in specified radix or default radix *); @ for_example @ public normal_example @ requires i == -34L; @ ensures \result != null && \result.equals("-34"); @*/ public static /*@ pure @*/ /*@ non_null @*/ String toString(long i, int radix); /*@ public normal_behavior @ {| @ old long mask_i = (long)(i + (2 << 64)); @ requires i < 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(1) != '0' @ && i == parseLong(\result, 16); @ ensures_redundantly \result.substring(1, \result.length()) @ .equals(toHexString(mask_i)); @ also @ requires i == 0; @ ensures \result != null && \result.length() == 1 @ && \result.charAt(0) == '0'; @ also @ requires i > 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(0) != '0' @ && i == parseLong(\result, 16); @ |} @ implies_that @ public normal_behavior @ ensures (* \result is a string representation of i in hexidecimal *); @*/ public static /*@ pure @*/ /*@ non_null @*/ String toHexString(long i); /*@ public normal_behavior @ {| @ old long mask_i = (long)(i + (2 << 64)); @ requires i < 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(1) != '0' @ && i == parseLong(\result, 8); @ ensures_redundantly \result.substring(1, \result.length()) @ .equals(toOctalString(mask_i)); @ also @ requires i == 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(0) == '0' @ && \result.length() == 1; @ also @ requires i > 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(0) != '0' @ && i == parseLong(\result, 8); @ |} @ implies_that @ public normal_behavior @ ensures (* \result is a string representation of i in octal *); @*/ public static /*@ pure @*/ /*@ non_null @*/ String toOctalString(long i); /*@ public normal_behavior @ {| @ old long mask_i = (long)(i + (2 << 64)); @ requires i < 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(1) != '0' @ && i == parseLong(\result, 2); @ ensures_redundantly \result.substring(1, \result.length()) @ .equals(toBinaryString(mask_i)); @ also @ requires i == 0; @ ensures \result != null && \result.length() == 1 @ && \result.charAt(0) == '0'; @ also @ requires i > 0; @ ensures \result != null && \result.length() >= 1 @ && \result.charAt(0) != '0' @ && i == parseLong(\result, 2); @ |} @ implies_that @ public normal_behavior @ ensures (* \result is a string representation of i in binary *); @*/ public static /*@ pure @*/ /*@ non_null @*/ String toBinaryString(long i); /*@ public normal_behavior @ ensures \result.equals(toString(i, 10)); @*/ public static /*@ pure @*/ /*@ non_null @*/ String toString(long i); /*@ public normal_behavior @ requires parseable(s, radix); @ ensures (* \result is the long of the string representation @ in the specified radix *); @ also @ public exceptional_behavior @ requires !parseable(s, radix); @ signals_only NumberFormatException; @ for_example @ public normal_example @ requires s.equals("342") && radix == 37; @ ensures \result == 342L; @ // radix was greater than MAX_RADIX so default to 10 @*/ public static /*@ pure @*/ long parseLong(String s, int radix) throws NumberFormatException; /*@ public normal_behavior @ requires parseable(s); @ ensures \result == parseLong(s, 10); @ also @ public exceptional_behavior @ requires !parseable(s); @ signals_only NumberFormatException; @*/ public static /*@ pure @*/ long parseLong(String s) throws NumberFormatException; /*@ public normal_behavior @ requires parseable(s, radix); @ ensures \fresh(\result); @ also @ public exceptional_behavior @ requires !parseable(s, radix); @ signals_only NumberFormatException; @*/ public static /*@ pure @*/ /*@ non_null @*/ Long valueOf(String s, int radix) throws NumberFormatException; /*@ public normal_behavior @ requires parseable(s); @ ensures \fresh(\result); @ also @ public exceptional_behavior @ requires !parseable(s); @ signals_only NumberFormatException; @*/ public static /*@ pure @*/ /*@ non_null @*/ Long valueOf(String s) throws NumberFormatException; /*@ public normal_behavior @ requires decodeable(nm); @ ensures (* \result is a Long representation of nm *); @ also @ public exceptional_behavior @ requires !decodeable(nm); @ signals(NumberFormatException); @*/ public static /*@ pure @*/ /*@ non_null @*/ Long decode(/*@non_null*/ String nm) throws NumberFormatException; /*@ public normal_behavior @ assignable theLong; @ ensures theLong == value; @*/ public Long(long value); /*@ public normal_behavior @ requires parseable(s); @ assignable theLong; @ ensures theLong == parseLong(s); @ also @ public exceptional_behavior @ requires !parseable(s); @ signals(NumberFormatException); @*/ public Long(String s) throws NumberFormatException; /*@ also @ public normal_behavior @ ensures \result == (byte) theLong; @*/ public byte byteValue(); /*@ also @ public normal_behavior @ ensures \result == (short) theLong; @*/ public short shortValue(); /*@ also @ public normal_behavior @ ensures \result == (int) theLong; @*/ public int intValue(); /*@ also @ public normal_behavior @ ensures \result == theLong; @*/ public long longValue(); /*@ also @ public normal_behavior @ ensures \result == (float) theLong; @*/ public float floatValue(); /*@ also @ public normal_behavior @ ensures \result == (double) theLong; @*/ public double doubleValue(); // specification inherited from Object public /*@ non_null @*/ String toString(); /*@ also @ public normal_behavior @ ensures \result == (int)(this.longValue()^(this.longValue()>>>32)) @ && (* \result is a hash code for theLong *); @*/ public int hashCode(); /*@ also @ public normal_behavior @ requires obj != null && (obj instanceof Long); @ ensures \result == (theLong == ((Long) obj).longValue()); @ also @ public normal_behavior @ requires obj == null || !(obj instanceof Long); @ ensures !\result; @*/ public boolean equals(/*@ nullable @*/ Object obj); /*@ public normal_behavior @ ensures \result.equals(getLong(nm, null)); @*/ public static /*@ pure @*/ /*@ non_null @*/ Long getLong(String nm); /*@ public normal_behavior @ ensures \result.equals(getLong(nm, new Long(val))); @*/ public static /*@ pure @*/ /*@ non_null @*/ Long getLong(String nm, long val); /*@ public normal_behavior @ requires nm != null && !nm.equals("") @ && System.getProperty(nm) != null @ && decodeable(System.getProperty(nm)); @ ensures \result.equals(decode(System.getProperty(nm))); @ also @ public normal_behavior @ requires nm == null || nm.equals("") @ || System.getProperty(nm) == null @ || !decodeable(System.getProperty(nm)); @ ensures \result.equals(val); @*/ //@ implies_that //@ ensures val != null ==> \result != null; public static /*@ pure @*/ /*@ non_null @*/ Long getLong(String nm, Long val); /*@ public normal_behavior @ requires anotherLong != null; @ {| @ requires theLong == anotherLong.longValue(); @ ensures \result == 0; @ also @ requires theLong < anotherLong.longValue(); @ ensures \result < 0; @ also @ requires theLong > anotherLong.longValue(); @ ensures \result > 0; @ |} @*/ public int compareTo(/*@ non_null @*/ Long anotherLong); /*@ also @ public normal_behavior @ requires o != null && (o instanceof Long); @ ensures \result == compareTo((Long) o); @ also @ public exceptional_behavior @ requires o == null && !(o instanceof Long); @ signals(ClassCastException); @*/ public int compareTo(/*@ non_null @*/ Object o); public static final /*@ non_null@*/ Class TYPE; }