org.jmlspecs.models
Class JMLArrayOps

java.lang.Object
  org.jmlspecs.models.JMLArrayOps

public class JMLArrayOps

extends Object

Array Operations that are useful for specifications.

Version:

$Revision: 1.12 $

Author:

Brandon Shilling, Gary T. Leavens

See Also:

Arrays, JMLObjectSequence, JMLValueSequence

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

JMLArrayOps()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
static boolean	hasObjectIdentity(non_null Object[] array, Object element)           Search the array for the given element and tell if that element's object identity occurs in the array.
static boolean	hasObjectIdentity(non_null Object[] array, Object element, int length)           Search the array for the given element and tell if that element's object identity occurs in the array from 0 the given length-1.
static boolean	hasValueEquals(non_null Object[] array, Object element)           Search the array for the given element and tell if an object with value "equals" to the given element occurs in the array.
static boolean	hasValueEquals(non_null Object[] array, Object element, int length)           Search the array for the given element and tell if an object with value "equals" to the given element occurs in the array from 0 the given length-1.
static int	objectIdentityCount(non_null Object[] array, Object element)           Search the array for the given element and return how many times that element's object identity occurs in the array.
static int	objectIdentityCount(non_null Object[] array, Object element, int length)           Search the array for the given element and return how many times that element's object identity occurs in the array from 0 the given length-1.
static int	valueEqualsCount(non_null Object[] array, Object element)           Search the array for the given element and return how many times an object with value "equals" to the given element occurs in the array.
static int	valueEqualsCount(non_null Object[] array, Object element, int length)           Search the array for the given element and return how many times an object with value "equals" to the given element occurs in the array from 0 the given length-1.

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

JMLArrayOps

public JMLArrayOps()

objectIdentityCount

public static int objectIdentityCount(non_null Object[] array,
                                      Object element)

Search the array for the given element and return how many times that element's object identity occurs in the array.

See Also:

objectIdentityCount(Object[], Object, int), hasObjectIdentity(Object[], Object), valueEqualsCount(Object[], Object)

Specifications: pure

public normal_behavior
requires array != null;
ensures \result == ( \num_of int i; 0 <= i&&i < array.length; array[i] == element);

objectIdentityCount

public static int objectIdentityCount(non_null Object[] array,
                                      Object element,
                                      int length)

Search the array for the given element and return how many times that element's object identity occurs in the array from 0 the given length-1.

See Also:

objectIdentityCount(Object[], Object), hasObjectIdentity(Object[], Object, int), valueEqualsCount(Object[], Object, int)

Specifications: pure

public normal_behavior
requires array != null;
requires 0 <= length&&length <= array.length;
ensures \result == ( \num_of int i; 0 <= i&&i < length; array[i] == element);

    implies_that

requires 0 <= length&&length <= array.length;

valueEqualsCount

public static int valueEqualsCount(non_null Object[] array,
                                   Object element)

Search the array for the given element and return how many times an object with value "equals" to the given element occurs in the array.

See Also:

valueEqualsCount(Object[], Object, int), hasValueEquals(Object[], Object), objectIdentityCount(Object[], Object)

Specifications: pure

public normal_behavior
requires array != null;
ensures \result == ( \num_of int i; 0 <= i&&i < array.length; (array[i] == null ==> element == null)&&(array[i] != null ==> (* array[i].equals(element) *)));

valueEqualsCount

public static int valueEqualsCount(non_null Object[] array,
                                   Object element,
                                   int length)

Search the array for the given element and return how many times an object with value "equals" to the given element occurs in the array from 0 the given length-1.

See Also:

valueEqualsCount(Object[], Object), hasValueEquals(Object[], Object, int), objectIdentityCount(Object[], Object, int)

Specifications: pure

public normal_behavior
requires array != null;
requires 0 <= length&&length <= array.length;
ensures \result == ( \num_of int i; 0 <= i&&i < length; (array[i] == null ==> element == null)&&(array[i] != null ==> (* array[i].equals(element) *)));

    implies_that

requires 0 <= length&&length <= array.length;

hasObjectIdentity

public static boolean hasObjectIdentity(non_null Object[] array,
                                        Object element)

Search the array for the given element and tell if that element's object identity occurs in the array.

See Also:

hasObjectIdentity(Object[], Object, int), objectIdentityCount(Object[], Object), hasValueEquals(Object[], Object)

Specifications: pure

public normal_behavior
requires array != null;
ensures \result == ( \exists int i; 0 <= i&&i < array.length; array[i] == element);

hasObjectIdentity

public static boolean hasObjectIdentity(non_null Object[] array,
                                        Object element,
                                        int length)

Search the array for the given element and tell if that element's object identity occurs in the array from 0 the given length-1.

See Also:

hasObjectIdentity(Object[], Object), objectIdentityCount(Object[], Object), hasValueEquals(Object[], Object)

Specifications: pure

public normal_behavior
requires array != null;
requires 0 <= length&&length <= array.length;
ensures \result == ( \exists int i; 0 <= i&&i < length; array[i] == element);

    implies_that

requires 0 <= length&&length <= array.length;

hasValueEquals

public static boolean hasValueEquals(non_null Object[] array,
                                     Object element)

Search the array for the given element and tell if an object with value "equals" to the given element occurs in the array.

See Also:

hasValueEquals(Object[], Object, int), valueEqualsCount(Object[], Object), hasObjectIdentity(Object[], Object)

Specifications: pure

public normal_behavior
requires array != null;
ensures \result == ( \exists int i; 0 <= i&&i < array.length; (array[i] == null ==> element == null)&&(array[i] != null ==> (* array[i].equals(element) *)));

hasValueEquals

public static boolean hasValueEquals(non_null Object[] array,
                                     Object element,
                                     int length)

Search the array for the given element and tell if an object with value "equals" to the given element occurs in the array from 0 the given length-1.

See Also:

hasValueEquals(Object[], Object), valueEqualsCount(Object[], Object, int), hasObjectIdentity(Object[], Object, int)

Specifications: pure

public normal_behavior
requires array != null;
requires 0 <= length&&length <= array.length;
ensures \result == ( \exists int i; 0 <= i&&i < length; (array[i] == null ==> element == null)&&(array[i] != null ==> (* array[i].equals(element) *)));

    implies_that

requires 0 <= length&&length <= array.length;