java.util
Class Arrays

java.lang.Object
  java.util.Arrays

public class Arrays

extends Object

JML's specification of java.util.Arrays.

Version:

$Revision: 1.9 $

Author:

Ajani Thomas, Gary T. Leavens

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

Arrays()

 

Model Method Summary
static boolean	equalElements(Object[] o, Object[] oo)

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
static List	asList(non_null Object[] a)
static int	binarySearch(byte[] a, byte key)
static int	binarySearch(char[] a, char key)
static int	binarySearch(double[] a, double key)
static int	binarySearch(float[] a, float key)
static int	binarySearch(int[] a, int key)
static int	binarySearch(Object[] a, Object key)
static int	binarySearch(Object[] a, Object key, nullable Comparator c)
static int	binarySearch(long[] a, long key)
static int	binarySearch(short[] a, short key)
static boolean	equals(nullable boolean[] a, nullable boolean[] a2)
static boolean	equals(nullable byte[] a, nullable byte[] a2)
static boolean	equals(nullable char[] a, nullable char[] a2)
static boolean	equals(nullable double[] a, nullable double[] a2)
static boolean	equals(nullable float[] a, nullable float[] a2)
static boolean	equals(nullable int[] a, nullable int[] a2)
static boolean	equals(nullable Object[] a, nullable Object[] a2)
static boolean	equals(nullable long[] a, nullable long[] a2)
static boolean	equals(nullable short[] a, nullable short[] a2)
static void	fill(boolean[] a, boolean val)
static void	fill(boolean[] a, int fromIndex, int toIndex, boolean val)
static void	fill(byte[] a, byte val)
static void	fill(byte[] a, int fromIndex, int toIndex, byte val)
static void	fill(char[] a, char val)
static void	fill(char[] a, int fromIndex, int toIndex, char val)
static void	fill(double[] a, double val)
static void	fill(double[] a, int fromIndex, int toIndex, double val)
static void	fill(float[] a, float val)
static void	fill(float[] a, int fromIndex, int toIndex, float val)
static void	fill(int[] a, int val)
static void	fill(int[] a, int fromIndex, int toIndex, int val)
static void	fill(Object[] a, int fromIndex, int toIndex, Object val)
static void	fill(Object[] a, Object val)
static void	fill(long[] a, int fromIndex, int toIndex, long val)
static void	fill(long[] a, long val)
static void	fill(short[] a, int fromIndex, int toIndex, short val)
static void	fill(short[] a, short val)
static void	sort(byte[] a)
static void	sort(byte[] a, int fromIndex, int toIndex)
static void	sort(char[] a)
static void	sort(char[] a, int fromIndex, int toIndex)
static void	sort(double[] a)
static void	sort(double[] a, int fromIndex, int toIndex)
static void	sort(float[] a)
static void	sort(float[] a, int fromIndex, int toIndex)
static void	sort(int[] a)
static void	sort(int[] a, int fromIndex, int toIndex)
static void	sort(Object[] a)
static void	sort(Object[] a, int fromIndex, int toIndex)
static void	sort(Object[] a, int fromIndex, int toIndex, nullable Comparator c)
static void	sort(Object[] a, nullable Comparator c)
static void	sort(long[] a)
static void	sort(long[] a, int fromIndex, int toIndex)
static void	sort(short[] a)
static void	sort(short[] a, int fromIndex, int toIndex)

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Constructor Detail

Arrays

public Arrays()

equalElements

public static boolean equalElements(Object[] o,
                                    Object[] oo)

Specifications: pure

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])));

sort

public static void sort(long[] a)

Specifications:

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 java.lang.NullPointerException;

sort

public static void sort(long[] a,
                        int fromIndex,
                        int toIndex)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

sort

public static void sort(int[] a)

Specifications:

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 java.lang.NullPointerException;

sort

public static void sort(int[] a,
                        int fromIndex,
                        int toIndex)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

sort

public static void sort(short[] a)

Specifications:

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 java.lang.NullPointerException;

sort

public static void sort(short[] a,
                        int fromIndex,
                        int toIndex)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

sort

public static void sort(char[] a)

Specifications:

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 java.lang.NullPointerException;

sort

public static void sort(char[] a,
                        int fromIndex,
                        int toIndex)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

sort

public static void sort(byte[] a)

Specifications:

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 java.lang.NullPointerException;

sort

public static void sort(byte[] a,
                        int fromIndex,
                        int toIndex)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

sort

public static void sort(double[] a)

Specifications:

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 java.lang.Double(a[i-1]).compareTo(new java.lang.Double(a[i])) <= 0);
ensures ( \forall int i; 0 <= i&&i < a.length; ( \num_of int j; 0 <= j&&j < a.length; new java.lang.Double(a[j]).compareTo(new java.lang.Double(a[i])) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); \old(new java.lang.Double(a[k])).compareTo(new java.lang.Double(a[i])) == 0));

     also

public exceptional_behavior
requires a == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

sort

public static void sort(double[] a,
                        int fromIndex,
                        int toIndex)

Specifications:

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 java.lang.Double(a[i-1]).compareTo(new java.lang.Double(a[i])) <= 0);
ensures ( \forall int i; 0 <= i&&i < a.length; ( \num_of int j; 0 <= j&&j < a.length; new java.lang.Double(a[j]).compareTo(new java.lang.Double(a[i])) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); \old(new java.lang.Double(a[k])).compareTo(new java.lang.Double(a[i])) == 0));

     also

public exceptional_behavior
requires a == null||fromIndex > toIndex||fromIndex < 0||toIndex > a.length;
assignable \nothing;
signals_only java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

sort

public static void sort(float[] a)

Specifications:

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 java.lang.Double(a[i-1]).compareTo(new java.lang.Double(a[i])) <= 0);
ensures ( \forall int i; 0 <= i&&i < a.length; ( \num_of int j; 0 <= j&&j < a.length; new java.lang.Double(a[j]).compareTo(new java.lang.Double(a[i])) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); \old(new java.lang.Double(a[k])).compareTo(new java.lang.Double(a[i])) == 0));

     also

public exceptional_behavior
requires a == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

sort

public static void sort(float[] a,
                        int fromIndex,
                        int toIndex)

Specifications:

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 java.lang.Float(a[i-1]).compareTo(new java.lang.Float(a[i])) <= 0);
ensures ( \forall int i; 0 <= i&&i < a.length; ( \num_of int j; 0 <= j&&j < a.length; new java.lang.Float(a[j]).compareTo(new java.lang.Float(a[i])) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); \old(new java.lang.Float(a[k])).compareTo(new java.lang.Float(a[i])) == 0));

     also

public exceptional_behavior
requires a == null||fromIndex > toIndex||fromIndex < 0||toIndex > a.length;
assignable \nothing;
signals_only java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

sort

public static void sort(Object[] a)

Specifications:

public normal_behavior
requires a != null;
requires ( \forall int i; 0 <= i&&i < a.length; a[i] instanceof java.lang.Comparable);
assignable a[*];
ensures_redundantly a.length == \old(a.length)&&a != null;
ensures ( \forall int i; 0 < i&&i < a.length; ((java.lang.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; ((java.lang.Comparable)a[j]).compareTo(a[i]) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); \old((java.lang.Comparable)a[k]).compareTo(a[i]) == 0));

     also

public exceptional_behavior
requires a == null||(* array contains elements not mutually comparable *);
assignable \nothing;
signals_only java.lang.NullPointerException, java.lang.ClassCastException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.ClassCastException) (* array contains elements not mutually comparable *);

sort

public static void sort(Object[] a,
                        int fromIndex,
                        int toIndex)

Specifications:

public normal_behavior
requires a != null;
requires ( \forall int i; 0 <= i&&i < a.length; a[i] instanceof java.lang.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; ((java.lang.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; ((java.lang.Comparable)a[j]).compareTo(a[i]) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); \old((java.lang.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 java.lang.NullPointerException, java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.ClassCastException) (* array contains elements not mutually comparable *);
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

sort

public static void sort(Object[] a,
                        nullable Comparator c)

Specifications:

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 java.lang.Comparable);
assignable a[*];
ensures_redundantly a.length == \old(a.length)&&a != null;
ensures ( \forall int i; 0 < i&&i < a.length; ((java.lang.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; ((java.lang.Comparable)a[j]).compareTo(a[i]) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); \old((java.lang.Comparable)a[k]).compareTo(a[i]) == 0));

     also

public exceptional_behavior
requires a == null||(* array contains elements not mutually comparable *);
assignable \nothing;
signals_only java.lang.NullPointerException, java.lang.ClassCastException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.ClassCastException) (* array contains elements not mutually comparable *);

sort

public static void sort(Object[] a,
                        int fromIndex,
                        int toIndex,
                        nullable Comparator c)

Specifications:

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 java.lang.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; ((java.lang.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; ((java.lang.Comparable)a[j]).compareTo(a[i]) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); \old((java.lang.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 java.lang.NullPointerException, java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.ClassCastException) (* array contains elements not mutually comparable *);
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

binarySearch

public static int binarySearch(long[] a,
                               long key)

Specifications: pure

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 java.lang.NullPointerException;

binarySearch

public static int binarySearch(int[] a,
                               int key)

Specifications: pure

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 java.lang.NullPointerException;

binarySearch

public static int binarySearch(short[] a,
                               short key)

Specifications: pure

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 java.lang.NullPointerException;

binarySearch

public static int binarySearch(char[] a,
                               char key)

Specifications: pure

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 java.lang.NullPointerException;

binarySearch

public static int binarySearch(byte[] a,
                               byte key)

Specifications: pure

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 java.lang.NullPointerException;

binarySearch

public static int binarySearch(double[] a,
                               double key)

Specifications: pure

public normal_behavior
requires a != null&&( \forall int i; 0 < i&&i < a.length; new java.lang.Double(a[i-1]).compareTo(new java.lang.Double(a[i])) <= 0);

{|

requires ( \exists int j; 0 <= j&&j < a.length; new java.lang.Double(a[j]).compareTo(new java.lang.Double(key)) == 0);
assignable \nothing;
ensures 0 <= \result &&\result < a.length&&new java.lang.Double(a[\result ]).compareTo(new java.lang.Double(key)) == 0;

also

requires !( \exists int j; 0 <= j&&j < a.length; new java.lang.Double(a[j]).compareTo(new java.lang.Double(key)) == 0);
assignable \nothing;
ensures \result < 0;
ensures ( \exists int j; 0 <= j&&j < a.length; new java.lang.Double(a[j]).compareTo(new java.lang.Double(key)) < 0) ==> new java.lang.Double(a[(\result *-1)-2]).compareTo(new java.lang.Double(key)) < 0;
ensures ((\result *-1)-1 < a.length&&new java.lang.Double(a[(\result *-1)-1]).compareTo(new java.lang.Double(key)) > 0)||(\result *-1)-1 == a.length;
ensures_redundantly ( \exists int j; 0 <= j&&j < a.length; new java.lang.Double(a[j]).compareTo(new java.lang.Double(key)) > 0) ==> new java.lang.Double(a[(\result *-1)-1]).compareTo(new java.lang.Double(key)) > 0;

|}

     also

public exceptional_behavior
requires a == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

binarySearch

public static int binarySearch(float[] a,
                               float key)

Specifications: pure

public normal_behavior
requires a != null&&( \forall int i; 0 < i&&i < a.length; new java.lang.Float(a[i-1]).compareTo(new java.lang.Float(a[i])) <= 0);

{|

requires ( \exists int j; 0 <= j&&j < a.length; new java.lang.Float(a[j]).compareTo(new java.lang.Float(key)) == 0);
assignable \nothing;
ensures 0 <= \result &&\result < a.length&&new java.lang.Float(a[\result ]).compareTo(new java.lang.Float(key)) == 0;

also

requires !( \exists int j; 0 <= j&&j < a.length; new java.lang.Float(a[j]).compareTo(new java.lang.Float(key)) == 0);
assignable \nothing;
ensures \result < 0;
ensures ( \exists int j; 0 <= j&&j < a.length; new java.lang.Float(a[j]).compareTo(new java.lang.Float(key)) < 0) ==> new java.lang.Float(a[(\result *-1)-2]).compareTo(new java.lang.Float(key)) < 0;
ensures ((\result *-1)-1 < a.length&&new java.lang.Float(a[(\result *-1)-1]).compareTo(new java.lang.Float(key)) > 0)||(\result *-1)-1 == a.length;
ensures_redundantly ( \exists int j; 0 <= j&&j < a.length; new java.lang.Float(a[j]).compareTo(new java.lang.Float(key)) > 0) ==> new java.lang.Float(a[(\result *-1)-1]).compareTo(new java.lang.Float(key)) > 0;

|}

     also

public exceptional_behavior
requires a == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

binarySearch

public static int binarySearch(Object[] a,
                               Object key)

Specifications: pure

public normal_behavior
requires a != null;
requires ( \forall int i; 0 <= i&&i < a.length; a[i] instanceof java.lang.Comparable)&&key instanceof java.lang.Comparable;
requires ( \forall int i; 0 < i&&i < a.length; ((java.lang.Comparable)a[i-1]).compareTo(a[i]) <= 0);

{|

requires ( \exists int j; 0 <= j&&j < a.length; ((java.lang.Comparable)a[j]).compareTo(key) == 0);
assignable \nothing;
ensures 0 <= \result &&\result < a.length&&((java.lang.Comparable)a[\result ]).compareTo(key) == 0;

also

requires !( \exists int j; 0 <= j&&j < a.length; ((java.lang.Comparable)a[j]).compareTo(key) == 0);
assignable \nothing;
ensures \result < 0;
ensures ( \exists int j; 0 <= j&&j < a.length; ((java.lang.Comparable)a[j]).compareTo(key) < 0) ==> ((java.lang.Comparable)a[(\result *-1)-2]).compareTo(key) < 0;
ensures ((\result *-1)-1 < a.length&&((java.lang.Comparable)a[(\result *-1)-1]).compareTo(key) > 0)||(\result *-1)-1 == a.length;
ensures_redundantly ( \exists int j; 0 <= j&&j < a.length; ((java.lang.Comparable)a[j]).compareTo(key) > 0) ==> ((java.lang.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 java.lang.NullPointerException, java.lang.ClassCastException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.ClassCastException) (* array contains elements not comparable to key *);

binarySearch

public static int binarySearch(Object[] a,
                               Object key,
                               nullable Comparator c)

Specifications: pure

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 java.lang.Comparable)&&key instanceof java.lang.Comparable;
requires ( \forall int i; 0 < i&&i < a.length; ((java.lang.Comparable)a[i-1]).compareTo(a[i]) <= 0);

{|

requires ( \exists int j; 0 <= j&&j < a.length; ((java.lang.Comparable)a[j]).compareTo(key) == 0);
assignable \nothing;
ensures 0 <= \result &&\result < a.length&&((java.lang.Comparable)a[\result ]).compareTo(key) == 0;

also

requires !( \exists int j; 0 <= j&&j < a.length; ((java.lang.Comparable)a[j]).compareTo(key) == 0);
assignable \nothing;
ensures \result < 0;
ensures ( \exists int j; 0 <= j&&j < a.length; ((java.lang.Comparable)a[j]).compareTo(key) < 0) ==> ((java.lang.Comparable)a[(\result *-1)-2]).compareTo(key) < 0;
ensures ((\result *-1)-1 < a.length&&((java.lang.Comparable)a[(\result *-1)-1]).compareTo(key) > 0)||(\result *-1)-1 == a.length;
ensures_redundantly ( \exists int j; 0 <= j&&j < a.length; ((java.lang.Comparable)a[j]).compareTo(key) > 0) ==> ((java.lang.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 java.lang.NullPointerException, java.lang.ClassCastException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.ClassCastException) (* array contains elements not comparable to key *);

equals

public static boolean equals(nullable long[] a,
                             nullable long[] a2)

Specifications: pure

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]);

equals

public static boolean equals(nullable int[] a,
                             nullable int[] a2)

Specifications: pure

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]);

equals

public static boolean equals(nullable short[] a,
                             nullable short[] a2)

Specifications: pure

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]);

equals

public static boolean equals(nullable char[] a,
                             nullable char[] a2)

Specifications: pure

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]);

equals

public static boolean equals(nullable byte[] a,
                             nullable byte[] a2)

Specifications: pure

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]);

equals

public static boolean equals(nullable boolean[] a,
                             nullable boolean[] a2)

Specifications: pure

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]);

equals

public static boolean equals(nullable double[] a,
                             nullable double[] a2)

Specifications: pure

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 java.lang.Double(a[i]).equals(new java.lang.Double(a2[i])));

equals

public static boolean equals(nullable float[] a,
                             nullable float[] a2)

Specifications: pure

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 java.lang.Float(a[i]).equals(new java.lang.Float(a2[i])));

equals

public static boolean equals(nullable Object[] a,
                             nullable Object[] a2)

Specifications: pure

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]));

fill

public static void fill(long[] a,
                        long val)

Specifications:

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 java.lang.NullPointerException;

fill

public static void fill(long[] a,
                        int fromIndex,
                        int toIndex,
                        long val)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

fill

public static void fill(int[] a,
                        int val)

Specifications:

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 java.lang.NullPointerException;

fill

public static void fill(int[] a,
                        int fromIndex,
                        int toIndex,
                        int val)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

fill

public static void fill(short[] a,
                        short val)

Specifications:

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 java.lang.NullPointerException;

fill

public static void fill(short[] a,
                        int fromIndex,
                        int toIndex,
                        short val)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

fill

public static void fill(char[] a,
                        char val)

Specifications:

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 java.lang.NullPointerException;

fill

public static void fill(char[] a,
                        int fromIndex,
                        int toIndex,
                        char val)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

fill

public static void fill(byte[] a,
                        byte val)

Specifications:

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 java.lang.NullPointerException;

fill

public static void fill(byte[] a,
                        int fromIndex,
                        int toIndex,
                        byte val)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

fill

public static void fill(boolean[] a,
                        boolean val)

Specifications:

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 java.lang.NullPointerException;

fill

public static void fill(boolean[] a,
                        int fromIndex,
                        int toIndex,
                        boolean val)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

fill

public static void fill(double[] a,
                        double val)

Specifications:

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 java.lang.Double(a[i]).compareTo(new java.lang.Double(val)) == 0);

     also

public exceptional_behavior
requires a == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

fill

public static void fill(double[] a,
                        int fromIndex,
                        int toIndex,
                        double val)

Specifications:

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 java.lang.Double(a[i]).compareTo(new java.lang.Double(val)) == 0);
ensures ( \forall int i; 0 <= i&&i < a.length; ( \num_of int j; 0 <= j&&j < fromIndex; new java.lang.Double(a[j]).compareTo(new java.lang.Double(a[i])) == 0) == ( \num_of int k; 0 <= k&&k < fromIndex; new java.lang.Double(\old(a[k])).compareTo(new java.lang.Double(a[i])) == 0));
ensures ( \forall int i; 0 <= i&&i < a.length; ( \num_of int j; toIndex <= j&&j < a.length; new java.lang.Double(a[j]).compareTo(new java.lang.Double(a[i])) == 0) == ( \num_of int k; toIndex <= k&&k < \old(a.length); new java.lang.Double(\old(a[k])).compareTo(new java.lang.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 java.lang.Double(a[j]).compareTo(new java.lang.Double(a[i])) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); new java.lang.Double(\old(a[k])).compareTo(new java.lang.Double(a[i])) == 0));

     also

public exceptional_behavior
requires a == null||fromIndex > toIndex||fromIndex < 0||toIndex > a.length;
assignable \nothing;
signals_only java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

fill

public static void fill(float[] a,
                        float val)

Specifications:

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 java.lang.Float(a[i]).compareTo(new java.lang.Float(val)) == 0);

     also

public exceptional_behavior
requires a == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

fill

public static void fill(float[] a,
                        int fromIndex,
                        int toIndex,
                        float val)

Specifications:

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 java.lang.Float(a[i]).compareTo(new java.lang.Float(val)) == 0);
ensures ( \forall int i; 0 <= i&&i < a.length; ( \num_of int j; 0 <= j&&j < fromIndex; new java.lang.Float(a[j]).compareTo(new java.lang.Float(a[i])) == 0) == ( \num_of int k; 0 <= k&&k < fromIndex; new java.lang.Float(\old(a[k])).compareTo(new java.lang.Float(a[i])) == 0));
ensures ( \forall int i; 0 <= i&&i < a.length; ( \num_of int j; toIndex <= j&&j < a.length; new java.lang.Float(a[j]).compareTo(new java.lang.Float(a[i])) == 0) == ( \num_of int k; toIndex <= k&&k < \old(a.length); new java.lang.Float(\old(a[k])).compareTo(new java.lang.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 java.lang.Float(a[j]).compareTo(new java.lang.Float(a[i])) == 0) == ( \num_of int k; 0 <= k&&k < \old(a.length); new java.lang.Float(\old(a[k])).compareTo(new java.lang.Float(a[i])) == 0));

     also

public exceptional_behavior
requires a == null||fromIndex > toIndex||fromIndex < 0||toIndex > a.length;
assignable \nothing;
signals_only java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

fill

public static void fill(Object[] a,
                        Object val)

Specifications:

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 java.lang.NullPointerException;

fill

public static void fill(Object[] a,
                        int fromIndex,
                        int toIndex,
                        Object val)

Specifications:

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 java.lang.NullPointerException, java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
signals (java.lang.NullPointerException) a == null;
signals (java.lang.IllegalArgumentException) fromIndex > toIndex;
signals (java.lang.ArrayIndexOutOfBoundsException) fromIndex < 0||toIndex > a.length;

asList

public static List asList(non_null Object[] a)

Specifications: non_null

public normal_behavior
assignable \nothing;
ensures \result .theList.equals(org.jmlspecs.models.JMLEqualsSequence.convertFrom(a));