/**
  * Copyright (c): Uwe Schmidt, FH Wedel
  *
  * You may study, modify and distribute this source code
  * FOR NON-COMMERCIAL PURPOSES ONLY.
  * This copyright message has to remain unchanged.
  *
  * Note that this document is provided 'as is',
  * WITHOUT WARRANTY of any kind either expressed or implied.
  */

/**
 * @author Uwe Schmidt
 *
 * predicates and functions on arrays of integers
 *
 * the startup class
 *
 */

//--------------------

class Field {

  public static
  void main(String[] args) {

    // a 1. test case
    {
      long [] a1 = {};
      Array   f1 = new Array(a1);

      f1.testCases("f1");
    }

    // a 2. test case
    {
      long [] a2 = {1};
      Array   f2 = new Array(a2);

      f2.testCases("f2");
    }
    // a 3. test case
    {
      long [] a3 = {1, 100, 40, 40, 100, 3};
      Array   f3 = new Array(a3);

      f3.testCases("f3");
    }
  }
}

//--------------------

/**
 * predicates and functions for arrays of integers
 *
 */

class Array {

  /*
   * the field variable f
   */

  private
  long [] f;

  //--------------------
  /**
   * the constructor: initialization of f.
   */

  public
  Array(long [] f) {
    this.f = f;
  }

  //--------------------
  /**
   * access element i.
   */

  public
  long at(int i) {
    return
      f[i];
  }

  //--------------------
  /**
   * modification at position i.
   */

  public
  void putAt(int i, long v) {
    f[i] = v;
  }

  //--------------------
  /**
   * search function.
   * Returns true if v is found in field f
   */

  public
  boolean contains(long v) {
    return
      contains(v, f.length);
  }

  //--------------------
  /**
   * search function.
   * returns true if v is found in the first n elements of f
   * specification:
   *   exists 0 <= i < n : f[i] = v
   * implemented as linear search loop
   */

  public
  boolean contains(long v,
		   int n) {
    int i = 0;

    while ( i < n && f[i] != v ) {
      i = i + 1;
    }

    return
      i < n;
  }

  //--------------------
  /**
   * all elements equal.
   */

  public
  boolean allEqual() {
    return
      allEqual(f.length);
  }

  //--------------------
  /**
   * all first n elements equal.
   * specification:
   *   forall 0 < i < n : f[i-1] = f[i]
   */

  public
  boolean allEqual(int n) {
    int i = 1;
    boolean equal = true;

    while ( equal && i < n ) {
      equal = f[i-1] == f[i];
      i = i + 1;
    }

    return
      equal;
  }

  //--------------------
  /**
   * all elements less than or equal to a value.
   */

  public
  boolean allLessThanOrEqualTo(long m) {
    return
      allLessThanOrEqualTo(m, f.length);
  }

  //--------------------
  /**
   * all first n elements less than or equal to a value.
   * specification:
   *   forall 0 <= i < n : f[i] <= m
   * implemented as linear search:
   *   not (exists 0 <= i < n : f[i] > m)
   */

  public
  boolean allLessThanOrEqualTo(long m,
			       int n) {
    int i = 0;

    while ( i < n && f[i] <= m) {
      i = i + 1;
    }

    return
      i == n;
  }


  //--------------------
  /**
   * all elements except one special value
   * less than or equal to a given value.
   */

  public
  boolean allExceptOneLessThanOrEqualTo(long m2,
					long m) {
    return
      allExceptOneLessThanOrEqualTo(m2,m,f.length);
  }

  //--------------------
  /**
   * all first n elements except one special value
   * less than or equal to a given value.
   * specification:
   *   forall 0 <= i < n : f[i] != m => f[i] <= m2
   */

  public boolean allExceptOneLessThanOrEqualTo(long m2,
					       long m,
					       int n) {
    int     i = 0;
    boolean r = true;

    while ( r && i < n ) {
      r = (f[i] == m) || (f[i] <= m2);
      i = i + 1;
    }

    return r;
  }


  //--------------------
  /**
   * greatest element in f.
   */

  public long max() {
    return
      max(f.length);
  }

  //--------------------
  /**
   * greatest of first n elements.
   * specification:
   *   exist 0 <= i < n : f[i] = max
   *   and
   *   forall 0 <= i < n : f[i] <= max
   * precondition: checked by array index check
   *   0 < n
   */

  public long max(int n) {
    int i = 1;
    long m = f[0];

    while ( i < n ) {
      m = f[i] > m ? f[i] : m;
      i = i + 1;
    }

    return m;
  }

  //--------------------
  /**
   * second greatest element in f.
   */

  public long max2() {
    return
      max2(f.length);
  }

  //--------------------
  /**
   * second greatest of first n elements.
   * specification:
   *   max = f.max(n)
   *   and
   *   f.contains(max2)
   *   and
   *   not f.allEqual(n)
   *     => (forall 0 <= i < n : f[i] != max => f[i] <= max2)
   *
   * if more than 1 values are stored in f,
   * the 2. greatest is returned, else
   * the value occuring in f is returned
   * precondition:
   *   interval contains at least 1 element
   * 0 < n
   */

  public
  long max2(int n) {
    int	    i        = 1;
    long    max      = f[0];
    long    max2     = max;	// max == max2 --> all elements equal

    while ( i < n ) {
      // 3 cases: f[i] > max, f[i] < max, f[i] == max

      if ( f[i] > max ) { // 1. case
	max2 = max;
	max  = f[i];
      }
      else
      if ( f[i] < max ) {
	// 2. case
	if ( max == max2 ) {
	  // a 2. value found, it's less than max
	  max2 = f[i];
	}
	else {
	  // already 2 values found, test whether new max2 found
	  if ( f[i] > max2 ) {
	    max2 = f[i];
	  }
	}
      }
      else {
	// 3. case: f[i] == max
	// nothing changes
      }
      i = i + 1;
    }

    return max2;
  }

  //--------------------
  /**
   * the String conversion routine
   */

  public
  String toString() {
    if (f.length == 0)
      return
	"{}";
    else {
      String r = "{";

      for (int i = 0;
	   i < f.length;
	   ++i) {
	r = r + f[i] + (i < f.length -1 ? "," : "}");
      }

      return r;
    }
  }

  //--------------------
  /**
   * a few test cases
   */

  public
  void testCases(String n) {
    System.out.println("Array " + n + " = " + toString());
    System.out.println(n + ".length = " + f.length);
    System.out.println(n + ".contains(0) = " + contains(0));
    System.out.println(n + ".contains(1) = " + contains(1));
    System.out.println(n + ".allEqual() = " + allEqual());

    if (f.length != 0) {
      System.out.println(n + ".max() = " + max());
      System.out.println(n + ".max2() = " + max2());
      System.out.println(n + ".max() == " + n + ".max2() = " +
			 (max() == max2()));
      System.out.println(n + ".contains(" + f[0] + ") = " + contains(f[0]));
      System.out.println(n + ".contains(" + max() + ") = " + contains(max()));
      System.out.println(n + ".contains(" + max2() + ") = " + contains(max2()));
      System.out.println(n + ".allLessThanOrEqualTo(" + f[0] + ") = " +
			 allLessThanOrEqualTo(f[0]));
      System.out.println(n + ".allLessThanOrEqualTo(" + max() + ") = " +
			 allLessThanOrEqualTo(max()));
      System.out.println(n + ".allLessThanOrEqualTo(" + max2() + ") = " +
			 allLessThanOrEqualTo(max2()));
      System.out.println(n + ".allExceptOneLessThanOrEqualTo(" + max2() + "," + max() + ") = " +
			 allExceptOneLessThanOrEqualTo(max2(),max()));
      System.out.println(n + ".allExceptOneLessThanOrEqualTo(" + max() + "," + max2() + ") = " +
			 allExceptOneLessThanOrEqualTo(max(),max2()));
    }
    System.out.println("");
  }

}

//--------------------