// @(#)$Id: Integer.jml,v 1.21 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.Integer.
 * @version $Revision: 1.21 $
 * @author Brandon Shilling
 * @author Gary T. Leavens
 */
//-@ immutable
public  /*@ pure @*/ final
    class Integer extends Number implements Comparable {

    //@ public model int theInteger;
    //@ public represents theInteger <- intValue();

    /*@ 

    @   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 int, 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 int   MIN_VALUE;

    public static final int   MAX_VALUE;

    public static final /*@non_null@*/ Class TYPE;

    final static /*@non_null@*/ char[] digits;

    /*@ 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 == parseInt(\result, radix);
      @   also
      @     requires i > 0;
      @     ensures \result != null && \result.length() >= 1
      @         && \result.charAt(0) != '0'
      @         && i == parseInt(\result, radix);
      @   also
      @     requires i == 0;
      @     ensures "0".equals(\result);
      @   |}
      @  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 == parseInt(\result, 10);
      @   also
      @     requires i > 0;
      @     ensures \result!= null && \result.length() >= 1
      @         && \result.charAt(0) != '0'
      @         && i == parseInt(\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 == -34;
      @     ensures \result != null && \result.equals("-34"); 
      @*/
    public static /*@ pure @*/ /*@ non_null @*/ String toString(int i,
                                                                  int radix);

    /*@ public normal_behavior
      @  {|
      @   old int mask_i = (int)(i + (1L << 32));
      @   requires i < 0 && i != MIN_VALUE;
      @   ensures \result != null && \result.length() >= 1
      @         && \result.charAt(1) != '0' ;
      @   ensures \result.equals(toHexString(mask_i));
      @  also
      @   requires i == MIN_VALUE;
      @   ensures \result.equals("80000000");
      @  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 == parseInt(\result, 16);
      @ |}
      @ implies_that
      @   public normal_behavior
      @   ensures (* \result is a string representation of i in hexidecimal *);
      @*/
    public static /*@ pure @*/ /*@ non_null @*/ String toHexString(int i);

    /*@ public normal_behavior
      @  {|
      @   old int mask_i = (int)(i + (1L << 32));
      @   requires i < 0 && i != MIN_VALUE; 
      @   ensures \result != null && \result.length() >= 1
      @         && \result.charAt(1) != '0'; 
      @   ensures \result.equals(toOctalString(mask_i));
      @  also
      @   requires i == MIN_VALUE;
      @   ensures \result.equals("20000000000");
      @ 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 == parseInt(\result, 8);
      @ |}
      @ implies_that
      @   public normal_behavior
      @     ensures (* \result is a string representation of i in octal *);
      @*/
    public static /*@ pure @*/ /*@ non_null @*/ String toOctalString(int i);

    /*@ public normal_behavior
      @  {|
      @   old int mask_i = (int)(i + (1L << 32));
      @   requires i < 0 && i != MIN_VALUE;
      @   ensures \result != null && \result.length() >= 1
      @         && \result.charAt(1) != '0' ;
      @   ensures \result.equals(toBinaryString(mask_i));
      @  also
      @   requires i == MIN_VALUE;
      @   ensures \result.equals("10000000000000000000000000000000");
      @  also
      @   requires i == 0;
      @   ensures "0".equals(\result);
      @  also
      @   requires i > 0;
      @   ensures \result != null && \result.length() >= 1
      @         && \result.charAt(0) != '0'
      @         && i == parseInt(\result, 2);
      @ |}
      @ implies_that
      @   public normal_behavior
      @     ensures (* \result is a string representation of i in binary *);
      @*/
    public static /*@ pure @*/ /*@ non_null @*/ String toBinaryString(int i);
            
    final static /*@non_null@*/ char [] DigitTens;

    final static /*@non_null@*/ char [] DigitOnes;

    /*@ public normal_behavior
      @   ensures \result.equals(toString(i, 10));
      @*/
    public static /*@ pure @*/ /*@ non_null @*/ String toString(int i);

    /*@  public normal_behavior
      @    requires parseable(s, radix);
      @    ensures (* \result is the int of the string representation
      @               in the specified radix *);
      @ also 
      @ public exceptional_behavior
      @   requires !parseable(s, radix);
      @   signals_only NumberFormatException;
      @*/
    public static /*@ pure @*/ int parseInt(String s, int radix)
        throws NumberFormatException;
                
    /*@    public normal_behavior
      @      requires parseable(s);
      @      ensures \result == parseInt(s, 10);
      @ also
      @    public exceptional_behavior
      @      requires !parseable(s);
      @      signals_only NumberFormatException;
      @*/
    public static /*@ pure @*/ int parseInt(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 @*/
        Integer 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 @*/ Integer valueOf(String s)
        throws NumberFormatException;

    /*@ public normal_behavior
      @   assignable theInteger;
      @   ensures theInteger == value;
      @*/
    public Integer(int value);
    
    /*@ public normal_behavior
      @   requires parseable(s);
      @   assignable theInteger;
      @   ensures theInteger == parseInt(s);
      @ also
      @ public exceptional_behavior
      @   requires !parseable(s);
      @   signals(NumberFormatException);
      @*/
    public Integer(String s) throws NumberFormatException ;
 
    /*@ also
      @   public normal_behavior
      @     ensures \result == (byte) theInteger;
      @*/
    public byte byteValue();
    
    /*@ also
      @   public normal_behavior
      @     ensures \result == (short) theInteger;
      @*/
    public short shortValue();

    /*@ also
      @   public normal_behavior
      @     ensures \result == theInteger;
      @*/
    public /*@ pure @*/ int intValue();
    
    /*@ also
      @   public normal_behavior
      @     ensures \result == (long) theInteger;
      @*/
    public long longValue();
    
    /*@ also
      @   public normal_behavior
      @      ensures \result == (float) theInteger;
      @*/
    public float floatValue();
    
    /*@ also
      @   public normal_behavior
      @     ensures \result == (double) theInteger;
      @*/
    public double doubleValue();
    
    // specification inherited from Object
    public /*@ non_null @*/ String toString();
            
    /*@ also
      @   public normal_behavior
      @     ensures \result == theInteger;
      @*/
    public int hashCode();
   
    /*@ also
      @   public normal_behavior
      @     requires obj != null && (obj instanceof Integer);
      @     ensures \result == (theInteger == ((Integer) obj).intValue());
      @   also
      @   public normal_behavior
      @     requires obj == null || !(obj instanceof Integer);
      @     ensures !\result;
      @*/
    public boolean equals(/*@ nullable @*/ Object obj);
  
    /*@ public normal_behavior
      @   ensures (\result == null && getInteger(nm,null) == null) ||
      @           \result.equals(getInteger(nm, null));
      @*/
    public static /*@ pure @*/
        Integer getInteger(String nm);

    /*@ public normal_behavior
      @   ensures \result.equals(getInteger(nm, new Integer(val)));
      @*/
    public static /*@ pure @*/ 
        Integer getInteger(String nm, int 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 == val || \result.equals(val);
      @*/
    //@ implies_that
    //@    ensures val != null ==> \result != null;
    public static /*@ pure @*/ 
        Integer getInteger(String nm, Integer val);
    
    /*@ public normal_behavior
      @   requires decodeable(nm);
      @   ensures (* \result is a Integer representation of nm *);
      @ also
      @ public exceptional_behavior
      @   requires !decodeable(nm);
      @   signals(NumberFormatException);
      @*/
    public static /*@ pure @*/ /*@ non_null @*/
        Integer decode(/*@ non_null @*/ String nm)
        throws NumberFormatException;

    /*@ public normal_behavior
      @ requires anotherInteger != null;
      @ {|
      @   requires theInteger == anotherInteger.intValue();
      @   ensures \result == 0;
      @ also 
      @   requires theInteger < anotherInteger.intValue();
      @   ensures \result < 0;
      @ also
      @   requires theInteger > anotherInteger.intValue();
      @   ensures \result > 0;
      @ |}
      @*/
    public int compareTo(/*@ non_null @*/ Integer anotherInteger);
            
    /*@ also
      @   public normal_behavior
      @     requires o != null && (o instanceof Integer);
      @     ensures \result == compareTo((Integer) o);
      @ also
      @   public exceptional_behavior
      @     requires o == null && !(o instanceof Integer);
      @     signals(ClassCastException);
      @*/
    public int compareTo(/*@ non_null @*/ Object o);

}