// @(#)$Id: Arrays.refines-spec,v 1.9 2007/12/19 02:01:15 chalin 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.util;

//@ model import org.jmlspecs.models.*;

/** JML's specification of java.util.Arrays.
 * @version $Revision: 1.9 $
 * @author Ajani Thomas
 * @author Gary T. Leavens
 */
public class Arrays {

    /*@
      @ public normal_behavior
      @   ensures \result == ( o == oo ||
                 ( o != null && oo != null && o.length == oo.length &&
                   (\forall int i; 0<=i && i < o.length; o[i] == oo[i])));
      @
      @ public static pure model boolean equalElements(Object[] o, Object[] oo) {
          if (o == oo) return true;
          if (o == null || oo == null) return false;
          if (o.length != oo.length) return false;
          for (int i=0; i<o.length; ++i) {
            if (o[i] != oo[i]) return false;
          }
          return true;
        }
      @*/

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @           0 < i && i < a.length; a[i-1] <= a[i]);
      @   ensures (\forall int i; 0 <= i && i < a.length;
      @           (\num_of int j; 0 <= j && j < a.length;
      @            a[j] == a[i]) == 
      @           (\num_of int k; 0 <= k && k < \old(a.length);
      @                          \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null; 
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void sort(long[] a);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            a[i-1] <= a[i]);
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures (\forall int i; 0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @              a[j] == a[i]) 
      @              == 
      @              (\num_of int k; 0 <= k && k < \old(a.length);
      @                \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex 
      @            || fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(long[] a, int fromIndex, int toIndex);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 < i && i < a.length;
      @             a[i-1] <= a[i]);
      @   ensures (\forall int i; 0 <= i && i < a.length;
      @           (\num_of int j; 0 <= j && j < a.length; 

      @             a[j] == a[i])
      @           == 
      @           (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void sort(int[] a);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex < i && i < toIndex;
      @             a[i-1] <= a[i]);
      @   ensures (\forall int i;
      @             0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @              a[j] == a[i])
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @              \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @             fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(int[] a, int fromIndex, int toIndex);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 < i && i < a.length;
      @            a[i-1] <= a[i]);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             a[j] == a[i])
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null; 
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void sort(short[] a);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            a[i-1] <= a[i]);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             a[j] == a[i])
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @             fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(short[] a, int fromIndex, int toIndex);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 < i && i < a.length;
      @            a[i-1] <= a[i]);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             a[j] == a[i])
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null; 
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void sort(char[] a);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            a[i-1] <= a[i]);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             a[j] == a[i])
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(char[] a, int fromIndex, int toIndex);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 < i && i < a.length;
      @            a[i-1] <= a[i]);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             a[j] == a[i])
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null; 
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void sort(byte[] a);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            a[i-1] <= a[i]);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             a[j] == a[i])
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(byte[] a, int fromIndex, int toIndex);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 < i && i < a.length;
      @            new Double(a[i-1]).compareTo(new Double(a[i])) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @            new Double(a[j]).compareTo(new Double(a[i])) == 0)
      @           == 
      @           (\num_of int k; 0 <= k && k < \old(a.length);
      @            \old(new Double(a[k])).compareTo(new Double(a[i])) 
      @              == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void sort(double[] a);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            new Double(a[i-1]).compareTo(new Double(a[i])) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             new Double(a[j]).compareTo(new Double(a[i])) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(new Double(a[k])).compareTo(new Double(a[i])) 
      @                == 0));
      @ also
      @  public exceptional_behavior 
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException)  
      @             fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(double[] a, int fromIndex, int toIndex);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 < i && i < a.length;
      @            new Double(a[i-1]).compareTo(new Double(a[i])) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             new Double(a[j]).compareTo(new Double(a[i])) == 0)
      @            ==
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(new Double(a[k])).compareTo(new Double(a[i])) 
      @               == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void sort(float[] a);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            new Float(a[i-1]).compareTo(new Float(a[i])) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             new Float(a[j]).compareTo(new Float(a[i])) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(new Float(a[k])).compareTo(new Float(a[i])) 
      @                == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(float[] a, int fromIndex, int toIndex);

    /*@  public normal_behavior
      @   requires a != null;
      @   requires (\forall int i; 0 <= i && i < a.length; 
      @             a[i] instanceof Comparable);
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 < i && i < a.length;
      @            ((Comparable)a[i-1]).compareTo(a[i]) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             ((Comparable)a[j]).compareTo(a[i]) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old((Comparable)a[k]).compareTo(a[i]) == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null ||
      @     (* array contains elements not mutually comparable *);
      @   assignable \nothing;
      @   signals_only NullPointerException, ClassCastException; 
      @   signals (NullPointerException) a == null;
      @   signals (ClassCastException)
      @     (* array contains elements not mutually comparable *);
      @*/
    public static void sort(Object[] a);

    /*@  public normal_behavior
      @   requires a != null;
      @   requires (\forall int i; 0 <= i && i < a.length; 
      @              a[i] instanceof Comparable);
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            ((Comparable)a[i-1]).compareTo(a[i]) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             ((Comparable)a[j]).compareTo(a[i]) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old((Comparable)a[k]).compareTo(a[i]) == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length ||
      @      (* array contains elements not mutually comparable *);
      @   assignable \nothing;
      @   signals_only NullPointerException, ClassCastException,
      @               IllegalArgumentException, ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (ClassCastException)
      @           (* array contains elements not mutually comparable *);
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(Object[] a, int fromIndex, int toIndex);

    /*@  public normal_behavior
      @   requires a != null && c != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 < i && i < a.length;
      @            c.compare(a[i-1],a[i]) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             c.compare(a[j],a[i]) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             c.compare(\old(a[k]),a[i]) == 0));
      @ also
      @  public normal_behavior
      @   requires a != null && c == null;
      @   requires (\forall int i; 0 <= i && i < a.length; 
      @             a[i] instanceof Comparable);
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 < i && i < a.length;
      @            ((Comparable)a[i-1]).compareTo(a[i]) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             ((Comparable)a[j]).compareTo(a[i]) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old((Comparable)a[k]).compareTo(a[i]) == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null || 
      @     (* array contains elements not mutually comparable *);
      @   assignable \nothing;
      @   signals_only NullPointerException, ClassCastException;
      @   signals (NullPointerException) a == null;
      @   signals (ClassCastException)
      @     (* array contains elements not mutually comparable *);
      @*/
    public static void sort(Object[] a, /*@nullable*/ Comparator c);

    /*@  public normal_behavior
      @   requires a != null && c != null;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            c.compare(a[i-1],a[i]) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             c.compare(a[j],a[i]) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             c.compare(\old(a[k]),a[i]) == 0));
      @ also
      @  public normal_behavior
      @   requires a != null && c == null;
      @   requires (\forall int i; 0 <= i && i < a.length; 
      @             a[i] instanceof Comparable);
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            fromIndex < i && i < toIndex;
      @            ((Comparable)a[i-1]).compareTo(a[i]) <= 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             ((Comparable)a[j]).compareTo(a[i]) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old((Comparable)a[k]).compareTo(a[i]) == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length ||
      @     (* array contains elements not mutually comparable *);
      @   assignable \nothing;
      @   signals_only NullPointerException, ClassCastException,
      @               IllegalArgumentException, ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (ClassCastException)
      @     (* array contains elements not mutually comparable *);
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void sort(Object[] a, int fromIndex, int toIndex, /*@nullable*/ Comparator c);

    /*@  public normal_behavior
      @   requires a != null &&
      @            (\forall int i; 
      @             0 < i && i < a.length;
      @             a[i-1] <= a[i]); 
      @  {| 
      @     requires (\exists int j; 0 <= j && j < a.length; 
      @               a[j] == key);
      @     assignable \nothing;
      @     ensures 0 <= \result && \result < a.length 
      @           && a[\result] == key;
      @    also
      @     requires !(\exists int j; 0 <= j && j < a.length; 
      @                a[j] == key);
      @     assignable \nothing;
      @     ensures \result < 0;
      @     ensures (\exists int j; 0 <= j && j < a.length; 
      @              a[j] < key)
      @             ==> a[(\result*-1) - 2] < key;
      @     ensures ((\result*-1)-1 < a.length && 
      @              a[(\result*-1)-1] > key) 
      @              || (\result*-1)-1 == a.length; 
      @     ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @                          a[j] > key)
      @              ==> a[(\result*-1)-1] > key;
      @   |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static /*@ pure @*/ int binarySearch(long[] a, long key);

    /*@  public normal_behavior
      @   requires a != null &&
      @            (\forall int i; 
      @             0 < i && i < a.length;
      @             a[i-1] <= a[i]); 
      @  {| 
      @     requires (\exists int j; 0 <= j && j < a.length; 
      @               a[j] == key);
      @     assignable \nothing;
      @     ensures 0 <= \result && \result < a.length 
      @           && a[\result] == key;
      @    also
      @     requires !(\exists int j; 0 <= j && j < a.length; 
      @                a[j] == key);
      @     assignable \nothing;
      @     ensures \result < 0;
      @     ensures (\exists int j; 0 <= j && j < a.length; 
      @              a[j] < key)
      @             ==> a[(\result*-1) - 2] < key;
      @     ensures ((\result*-1)-1 < a.length && 
      @              a[(\result*-1)-1] > key) 
      @              || (\result*-1)-1 == a.length; 
      @     ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @                          a[j] > key)
      @              ==> a[(\result*-1)-1] > key;
      @   |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static /*@ pure @*/ int binarySearch(int[] a, int key);

    /*@  public normal_behavior
      @   requires a != null &&
      @            (\forall int i; 
      @             0 < i && i < a.length;
      @             a[i-1] <= a[i]); 
      @  {| 
      @     requires (\exists int j; 0 <= j && j < a.length; 
      @               a[j] == key);
      @     assignable \nothing;
      @     ensures 0 <= \result && \result < a.length 
      @           && a[\result] == key;
      @    also
      @     requires !(\exists int j; 0 <= j && j < a.length; 
      @                a[j] == key);
      @     assignable \nothing;
      @     ensures \result < 0;
      @     ensures (\exists int j; 0 <= j && j < a.length; 
      @              a[j] < key)
      @             ==> a[(\result*-1) - 2] < key;
      @     ensures ((\result*-1)-1 < a.length && 
      @              a[(\result*-1)-1] > key) 
      @              || (\result*-1)-1 == a.length; 
      @     ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @                          a[j] > key)
      @              ==> a[(\result*-1)-1] > key;
      @   |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static /*@ pure @*/ int binarySearch(short[] a, short key);

    /*@  public normal_behavior
      @   requires a != null &&
      @            (\forall int i; 
      @             0 < i && i < a.length;
      @             a[i-1] <= a[i]); 
      @  {| 
      @     requires (\exists int j; 0 <= j && j < a.length; 
      @               a[j] == key);
      @     assignable \nothing;
      @     ensures 0 <= \result && \result < a.length 
      @           && a[\result] == key;
      @    also
      @     requires !(\exists int j; 0 <= j && j < a.length; 
      @                a[j] == key);
      @     assignable \nothing;
      @     ensures \result < 0;
      @     ensures (\exists int j; 0 <= j && j < a.length; 
      @              a[j] < key)
      @             ==> a[(\result*-1) - 2] < key;
      @     ensures ((\result*-1)-1 < a.length && 
      @              a[(\result*-1)-1] > key) 
      @              || (\result*-1)-1 == a.length; 
      @     ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @                          a[j] > key)
      @              ==> a[(\result*-1)-1] > key;
      @   |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static /*@ pure @*/ int binarySearch(char[] a, char key);

    /*@  public normal_behavior
      @   requires a != null &&
      @            (\forall int i; 
      @             0 < i && i < a.length;
      @             a[i-1] <= a[i]); 
      @  {| 
      @     requires (\exists int j; 0 <= j && j < a.length; 
      @               a[j] == key);
      @     assignable \nothing;
      @     ensures 0 <= \result && \result < a.length 
      @           && a[\result] == key;
      @    also
      @     requires !(\exists int j; 0 <= j && j < a.length; 
      @                a[j] == key);
      @     assignable \nothing;
      @     ensures \result < 0;
      @     ensures (\exists int j; 0 <= j && j < a.length; 
      @              a[j] < key)
      @             ==> a[(\result*-1) - 2] < key;
      @     ensures ((\result*-1)-1 < a.length && 
      @              a[(\result*-1)-1] > key) 
      @              || (\result*-1)-1 == a.length; 
      @     ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @                          a[j] > key)
      @              ==> a[(\result*-1)-1] > key;
      @   |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static /*@ pure @*/ int binarySearch(byte[] a, byte key);

    /*@  public normal_behavior
      @   requires a != null &&
      @            (\forall int i;
      @             0 < i && i < a.length;
      @             new Double(a[i-1]).compareTo(new Double(a[i])) <= 0);
      @   {| 
      @      requires (\exists int j; 0 <= j && j < a.length;
      @                new Double(a[j]).compareTo(new Double(key)) == 0);
      @      assignable \nothing;
      @      ensures 0 <= \result && \result < a.length 
      @              && new Double(a[\result]).compareTo(new Double(key))
      @                     == 0;
      @     also
      @      requires !(\exists int j; 0 <= j && j < a.length; 
      @                 new Double(a[j]).compareTo(new Double(key)) == 0);
      @      assignable \nothing;
      @      ensures \result < 0;
      @      ensures (\exists int j; 0 <= j && j < a.length; 
      @               new Double(a[j]).compareTo(new Double(key)) < 0)
      @            ==> 
      @           new Double(a[(\result*-1)-2]).compareTo(new Double(key))
      @                < 0;
      @      ensures ((\result*-1)-1 < a.length && 
      @      new Double(a[(\result*-1)-1]).compareTo(new Double(key)) > 0)
      @              || (\result*-1)-1 == a.length; 
      @      ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @                   new Double(a[j]).compareTo(new Double(key)) > 0)
      @       ==> 
      @      new Double(a[(\result*-1)-1]).compareTo(new Double(key)) > 0;
      @    |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static /*@ pure @*/ int binarySearch(double[] a, double key);

    /*@  public normal_behavior
      @   requires a != null &&
      @            (\forall int i;
      @             0 < i && i < a.length;
      @             new Float(a[i-1]).compareTo(new Float(a[i])) <= 0);
      @   {| 
      @      requires (\exists int j; 0 <= j && j < a.length;
      @                new Float(a[j]).compareTo(new Float(key)) == 0);
      @      assignable \nothing;
      @      ensures 0 <= \result && \result < a.length 
      @              && new Float(a[\result]).compareTo(new Float(key))
      @                     == 0;
      @     also
      @      requires !(\exists int j; 0 <= j && j < a.length; 
      @                 new Float(a[j]).compareTo(new Float(key)) == 0);
      @      assignable \nothing;
      @      ensures \result < 0;
      @      ensures (\exists int j; 0 <= j && j < a.length; 
      @               new Float(a[j]).compareTo(new Float(key)) < 0)
      @            ==> 
      @           new Float(a[(\result*-1)-2]).compareTo(new Float(key))
      @                < 0;
      @      ensures ((\result*-1)-1 < a.length && 
      @      new Float(a[(\result*-1)-1]).compareTo(new Float(key)) > 0)
      @              || (\result*-1)-1 == a.length; 
      @      ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @                   new Float(a[j]).compareTo(new Float(key)) > 0)
      @       ==> 
      @      new Float(a[(\result*-1)-1]).compareTo(new Float(key)) > 0;
      @    |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static /*@ pure @*/ int binarySearch(float[] a, float key);

    /*@  public normal_behavior
      @   requires a != null; 
      @   requires (\forall int i; 0 <= i && i < a.length; 
      @             a[i] instanceof Comparable) && 
      @             key instanceof Comparable;
      @   requires (\forall int i;
      @             0 < i && i < a.length;
      @             ((Comparable)a[i-1]).compareTo(a[i]) <= 0);
      @   {| 
      @      requires (\exists int j; 0 <= j && j < a.length; 
      @                ((Comparable)a[j]).compareTo(key) == 0);
      @      assignable \nothing;
      @      ensures 0 <= \result && \result < a.length 
      @              && ((Comparable)a[\result]).compareTo(key) == 0;
      @     also
      @      requires !(\exists int j; 0 <= j && j < a.length; 
      @                ((Comparable)a[j]).compareTo(key) == 0);
      @      assignable \nothing;
      @      ensures \result < 0;
      @      ensures (\exists int j; 0 <= j && j < a.length; 
      @               ((Comparable)a[j]).compareTo(key) < 0)
      @       ==> ((Comparable)a[(\result*-1) - 2]).compareTo(key) < 0;
      @      ensures ((\result*-1)-1 < a.length && 
      @              ((Comparable)a[(\result*-1)-1]).compareTo(key) > 0)
      @               || (\result*-1)-1 == a.length; 
      @      ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @               ((Comparable)a[j]).compareTo(key) > 0)
      @       ==> ((Comparable)a[(\result*-1)-1]).compareTo(key) > 0;
      @    |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ||
      @            (* array contains elements not comparable to key *);
      @   assignable \nothing;
      @   signals_only NullPointerException, ClassCastException;
      @   signals (NullPointerException) a == null;
      @   signals (ClassCastException) 
      @            (* array contains elements not comparable to key *);
      @*/
    public static /*@ pure @*/ int binarySearch(Object[] a, Object key);

    /*@  public normal_behavior
      @   requires a != null && c != null;
      @   requires (\forall int i; 0 < i && i < a.length;
      @             c.compare(a[i-1],a[i]) <= 0);
      @   {| 
      @      requires (\exists int j; 0 <= j && j < a.length; 
      @                c.compare(a[j],key) == 0);
      @      assignable \nothing;
      @      ensures 0 <= \result && \result < a.length 
      @              && c.compare(a[\result],key) == 0;
      @     also
      @      requires !(\exists int j; 0 <= j && j < a.length; 
      @                 c.compare(a[j],key) == 0);
      @      assignable \nothing;
      @      ensures \result < 0;
      @      ensures (\exists int j; 0 <= j && j < a.length; 
      @               c.compare(a[j],key) < 0)
      @           ==> c.compare(a[(\result*-1) - 2],key) < 0;
      @      ensures ((\result*-1)-1 < a.length && 
      @               c.compare(a[(\result*-1)-1],key) > 0) 
      @               || (\result*-1)-1 == a.length; 
      @      ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @               c.compare(a[j],key) > 0)
      @           ==> c.compare(a[(\result*-1)-1],key) > 0;
      @    |}
      @ also
      @  public normal_behavior
      @   requires a != null && c == null;
      @   requires (\forall int i; 0 <= i && i < a.length; 
      @             a[i] instanceof Comparable) && 
      @             key instanceof Comparable;
      @   requires (\forall int i;
      @             0 < i && i < a.length;
      @             ((Comparable)a[i-1]).compareTo(a[i]) <= 0);
      @   {| 
      @      requires (\exists int j; 0 <= j && j < a.length;
      @               ((Comparable)a[j]).compareTo(key) == 0);
      @      assignable \nothing;
      @      ensures 0 <= \result && \result < a.length 
      @              && ((Comparable)a[\result]).compareTo(key) == 0;
      @     also
      @      requires !(\exists int j; 0 <= j && j < a.length; 
      @                ((Comparable)a[j]).compareTo(key) == 0);
      @      assignable \nothing;
      @      ensures \result < 0;
      @      ensures (\exists int j; 0 <= j && j < a.length; 
      @               ((Comparable)a[j]).compareTo(key) < 0)
      @       ==> ((Comparable)a[(\result*-1) - 2]).compareTo(key) < 0;
      @      ensures ((\result*-1)-1 < a.length && 
      @              ((Comparable)a[(\result*-1)-1]).compareTo(key) > 0) 
      @               || (\result*-1)-1 == a.length; 
      @      ensures_redundantly (\exists int j; 0 <= j && j < a.length;
      @               ((Comparable)a[j]).compareTo(key) > 0)
      @        ==> ((Comparable)a[(\result*-1)-1]).compareTo(key) > 0;
      @    |}
      @ also
      @  public exceptional_behavior
      @   requires a == null ||
      @            (* array contains elements not comparable to key *);
      @   assignable \nothing;
      @   signals_only NullPointerException, ClassCastException;
      @   signals (NullPointerException) a == null;
      @   signals (ClassCastException) 
      @            (* array contains elements not comparable to key *);
      @*/
    public static /*@ pure @*/ int binarySearch(Object[] a, Object key, /*@nullable*/ Comparator c);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @                   (\forall int i; 0 <= i && i < a.length; a[i] == a2[i]);
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ long[] a, /*@ nullable @*/ long[] a2);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @                   (\forall int i; 0 <= i && i < a.length; a[i] == a2[i]);
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ int[] a, /*@ nullable @*/ int[] a2);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @                   (\forall int i; 0 <= i && i < a.length; a[i] == a2[i]);
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ short[] a, /*@ nullable @*/ short[] a2);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @                   (\forall int i; 0 <= i && i < a.length; a[i] == a2[i]);
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ char[] a, /*@ nullable @*/ char[] a2);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @                   (\forall int i; 0 <= i && i < a.length; a[i] == a2[i]);
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ byte[] a, /*@ nullable @*/ byte[] a2);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @                   (\forall int i; 0 <= i && i < a.length; a[i] == a2[i]);
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ boolean[] a, /*@ nullable @*/ boolean[] a2);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @                    (\forall int i; 0 <= i && i < a.length;
      @                     new Double(a[i]).equals(new Double(a2[i])));
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ double[] a, /*@ nullable @*/ double[] a2);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @                    (\forall int i; 0 <= i && i < a.length;
      @                     new Float(a[i]).equals(new Float(a2[i])));
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ float[] a, /*@ nullable @*/ float[] a2);

    /*@  public normal_behavior
      @   requires a == null || a2 == null;
      @   ensures \result <==> a == a2;
      @ also 
      @  public normal_behavior
      @   requires a != null && a2 != null;
      @   ensures \result <==> a.length == a2.length && 
      @              (\forall int i; 0 <= i && i < a.length;
      @                a[i].equals(a2[i]));
      @*/
    public static /*@pure@*/ boolean equals(/*@ nullable @*/ Object[] a, /*@ nullable @*/ Object[] a2);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            a[i] == val);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(long[] a, long val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            a[i] == val);
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @      (\num_of int j; 0 <= j && j < a.length; 
      @       a[j] == a[i])
      @      == 
      @      (\num_of int k; 0 <= k && k < \old(a.length);
      @       \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(long[] a, int fromIndex, int toIndex, long val);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            a[i] == val);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(int[] a, int val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            a[i] == val);
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @      (\num_of int j; 0 <= j && j < a.length; 
      @       a[j] == a[i])
      @      == 
      @      (\num_of int k; 0 <= k && k < \old(a.length);
      @       \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(int[] a, int fromIndex, int toIndex, int val);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            a[i] == val);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(short[] a, short val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            a[i] == val);
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @      (\num_of int j; 0 <= j && j < a.length; 
      @       a[j] == a[i])
      @      == 
      @      (\num_of int k; 0 <= k && k < \old(a.length);
      @       \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(short[] a, int fromIndex, int toIndex, short val);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            a[i] == val);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(char[] a, char val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            a[i] == val);
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @      (\num_of int j; 0 <= j && j < a.length; 
      @       a[j] == a[i])
      @      == 
      @      (\num_of int k; 0 <= k && k < \old(a.length);
      @       \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(char[] a, int fromIndex, int toIndex, char val);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            a[i] == val);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(byte[] a, byte val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            a[i] == val);
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @      (\num_of int j; 0 <= j && j < a.length; 
      @       a[j] == a[i])
      @      == 
      @      (\num_of int k; 0 <= k && k < \old(a.length);
      @       \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(byte[] a, int fromIndex, int toIndex, byte val);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            a[i] == val);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(boolean[] a, boolean val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[fromIndex..toIndex-1];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            a[i] == val);
      @   ensures_redundantly (\forall int i;
      @            0 <= i && i < fromIndex  
      @            || toIndex <= i && i < a.length; 
      @                \old(a[i]) == a[i]);
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @      (\num_of int j; 0 <= j && j < a.length; 
      @       a[j] == a[i])
      @      == 
      @      (\num_of int k; 0 <= k && k < \old(a.length);
      @       \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(boolean[] a, int fromIndex, int toIndex, boolean val);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            new Double(a[i]).compareTo(new Double(val)) == 0);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(double[] a, double val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            new Double(a[i]).compareTo(new Double(val)) == 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < fromIndex; 
      @             new Double(a[j]).compareTo(new Double(a[i])) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < fromIndex;
      @      new Double(\old(a[k])).compareTo(new Double(a[i])) == 0));
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; toIndex <= j && j < a.length; 
      @             new Double(a[j]).compareTo(new Double(a[i])) == 0)
      @            == 
      @            (\num_of int k; toIndex <= k && k < \old(a.length);
      @       new Double(\old(a[k])).compareTo(new Double(a[i])) == 0));
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length;
      @             new Double(a[j]).compareTo(new Double(a[i])) == 0)
      @            ==
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @       new Double(\old(a[k])).compareTo(new Double(a[i])) == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(double[] a, int fromIndex, int toIndex, double val);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            new Float(a[i]).compareTo(new Float(val)) == 0);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(float[] a, float val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            new Float(a[i]).compareTo(new Float(val)) == 0);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < fromIndex; 
      @             new Float(a[j]).compareTo(new Float(a[i])) == 0)
      @            == 
      @            (\num_of int k; 0 <= k && k < fromIndex;
      @      new Float(\old(a[k])).compareTo(new Float(a[i])) == 0));
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; toIndex <= j && j < a.length; 
      @             new Float(a[j]).compareTo(new Float(a[i])) == 0)
      @            == 
      @            (\num_of int k; toIndex <= k && k < \old(a.length);
      @       new Float(\old(a[k])).compareTo(new Float(a[i])) == 0));
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length;
      @             new Float(a[j]).compareTo(new Float(a[i])) == 0)
      @            ==
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @       new Float(\old(a[k])).compareTo(new Float(a[i])) == 0));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(float[] a, int fromIndex, int toIndex, float val);

    /*@  public normal_behavior
      @   requires a != null;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; 0 <= i && i < a.length; 
      @            a[i] == val);
      @ also
      @  public exceptional_behavior
      @   requires a == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public static void fill(Object[] a, Object val);

    /*@  public normal_behavior
      @   requires a != null && fromIndex < toIndex;
      @   assignable a[*];
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i; fromIndex <= i && i < toIndex; 
      @            a[i] == val);
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @           (\num_of int j; 0 <= j && j < fromIndex; 
      @            a[j] == a[i])
      @           ==
      @           (\num_of int k; 0 <= k && k < fromIndex;
      @            \old(a[k]) == a[i]));
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; toIndex <= j && j < a.length; 
      @             a[j] == a[i])
      @            == 
      @            (\num_of int k; toIndex <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public normal_behavior
      @   requires a != null && fromIndex == toIndex;
      @   assignable \nothing;
      @   ensures_redundantly a.length == \old(a.length) && a != null;
      @   ensures (\forall int i;
      @            0 <= i && i < a.length;
      @            (\num_of int j; 0 <= j && j < a.length; 
      @             a[j] == a[i])
      @            == 
      @            (\num_of int k; 0 <= k && k < \old(a.length);
      @             \old(a[k]) == a[i]));
      @ also
      @  public exceptional_behavior
      @   requires a == null || fromIndex > toIndex ||
      @            fromIndex < 0 || toIndex > a.length;
      @   assignable \nothing;
      @   signals_only NullPointerException, IllegalArgumentException,
      @                ArrayIndexOutOfBoundsException;
      @   signals (NullPointerException) a == null;
      @   signals (IllegalArgumentException) fromIndex > toIndex;
      @   signals (ArrayIndexOutOfBoundsException) 
      @            fromIndex < 0 || toIndex > a.length;
      @*/
    public static void fill(Object[] a, int fromIndex, int toIndex, Object val);

    /*@  public normal_behavior
      @   assignable \nothing;
      @   ensures \result.theList.equals(JMLEqualsSequence.convertFrom(a));
      @*/
    public static /*@non_null*/ List asList(/*@non_null*/ Object[] a);
}