import java.util.Random;

/**
 * A simple class to experiment with the use of JML tools in Java program
 * verification. This class contains three simple array algorithms in static
 * methods, and a short main routine for testing them.
 *
 * @author Robi Malik
 */

public class ArrayTests
{

  /**
   * Searches an array of integers for an element.
   * @param  a       An array of integers. Must not be <CODE>null</CODE>.
   * @param  item    The number to be searched for.
   * @return The first position in the array <CODE>a</CODE> where the number
   *         <CODE>item</CODE> is stored, or the length of the array, it
   *         <CODE>item</CODE> is not contained.
   */
  /*@
    @ requires a != null;
    @ requires a.length >= 0;
    @ ensures \result >= 0;
    @ ensures \result <= a.length;
    @ ensures (\forall int i; i >= 0 && i < \result; a[i] != item);
    @ ensures (\exists int i; i >= 0 && i < a.length; a[i] == item) ==>
    @         a[\result] == item;
    @*/
  public static int sequentialSearch(final int[] a, final int item)
  {
    int index = 0;
    while (index < a.length && a[index] != item) {
      index++;
    }
    return index;
  }


  /**
   * Finds the maximum of an array of integers.
   * @param  a       An array of integers. Must not be <CODE>null</CODE>.
   * @return The largest number that appears in the array&nbsp;<CODE>a</CODE>.
   */
  /*@
    @ requires a != null;
    @ requires a.length >= 1;
    @ ensures (\forall int i; i >= 0 && i < a.length; a[i] <= \result);
    @ ensures (\exists int i; i >= 0 && i < a.length; a[i] == \result);
    @*/
  public static int findMaximum(final int[] a)
  {
    int index = 1;
    int max = a[0];
    while (index < a.length) {
      if (a[index] > max) {
        max = a[index];
      }
      index++;
    }
    return max;
  }


  /**
   * Sorts an array of integers.
   * This method uses a simple bubble-sort algorithm to sort the contents
   * of the input array in place. When the method returns the array is
   * sorted.
   * @param  a       The array to be sorted. Must not be <CODE>null</CODE>.
   */
  /*@
    @ requires a != null;
    @ requires a.length >= 0;
    @ ensures (\forall int i; i > 0 && i < a.length; a[i-1] <= a[i]);
    @*/
  public static void bubbleSort(final int[] a)
  {
    // must prove: INIT[start/0, sorted/false]
    int start = 0;
    boolean sorted = false;
    /*@ // INIT:
      @ assert start == 0;
      @ assert !sorted;
      @*/
    // must prove: INIT ==> INV1;
    /*@ // INV1:
      @ assert start >= 0;
      @ assert start <= a.length;
      @ assert (\forall int i; i > 0 && i < start; a[i-1] <= a[i]);
      @ assert sorted ==>
      @        (\forall int i; i > 0 && i < a.length; a[i-1] <= a[i]);
      @*/
    while (start < a.length && !sorted) {
      /*@ // COND1:
        @ assert start < a.length;
        @*/
      // must prove: INV1 && COND1 ==> COND1'[sorted/true, index/a.length-1]
      int index = a.length - 1;
      sorted = true;
      /*@ // COND1':
        @ assert start >= 0;
        @ assert start < a.length;
        @ assert index == a.length - 1;
        @ assert sorted;
        @ assert (\forall int i; i > 0 && i <= start; a[i-1] <= a[i]);
        @*/
      /*@ // All terms in inner loop in conjunction with ST:
        @ assert start >= 0;
        @ assert start < a.length;
        @ assert (\forall int i; i > 0 && i <= start; a[i-1] <= a[i]);
        @*/
      // must prove: COND1' ==> INV2 && ST;
      /*@ // INV2:
        @ assert start <= index;
        @ assert (\forall int i; i > index && i < a.length; a[index] <= a[i]);
        @ assert sorted ==>
        @        (\forall int i; i > index && i < a.length; a[i-1] <= a[i]);
        @*/
      while (index > start) {
        /*@ // COND2:
          @ assert start < index;
          @*/
        if (a[index] < a[index - 1]) {
          /*@ // IFCOND:
            @ assert a[index] < a[index-1];
            @*/
          // must prove: INV2 && COND2 && IFCOND && ST ==> IF0 && ST;
          /*@ // IF0:
            @ assert start < index;
            @ assert a[index] < a[index-1];
            @ assert (\forall int i; i > index && i < a.length;
            @                        a[index] <= a[i]);
            @*/
          // must prove: IF0 && ST ==> (IF1 && ST)[h/a[index]];
          final int h = a[index];
          /*@ // IF1:
            @ assert start < index;
            @ assert h < a[index-1];
            @ assert (\forall int i; i > index && i < a.length; h <= a[i]);
            @*/
          // must prove: IF1 && ST ==> (IF2 && ST)[a[index]/a[index-1]];
          a[index] = a[index - 1];
          /*@ // IF2:
            @ assert start < index;
            @ assert h < a[index];
            @ assert (\forall int i; i > index && i < a.length; h <= a[i]);
            @*/
          // must prove: IF2 && ST ==> IF2' && ST;
          /*@ // IF2':
            @ assert start < index;
            @ assert (\forall int i; i >= index && i < a.length; h <= a[i]);
            @*/
          // must prove: IF2 && ST ==> (IF3 && ST)[a[index-1]/h];
          a[index - 1] = h;
          /*@ // IF3:
            @ assert start < index;
            @ assert (\forall int i; i >= index && i < a.length;
            @                        a[index-1] <= a[i]);
            @*/
          // must prove: IF3 && ST ==> (IF4 && ST)[sorted/false];
          sorted = false;
          /*@ // IF4:
            @ assert start < index;
            @ assert (\forall int i; i >= index && i < a.length;
            @                        a[index-1] <= a[i]);
            @ assert !sorted;
            @*/
        }
        // must prove: INV2 && COND2 && !IFCOND && ST ==> INV2' && ST;
        // must prove: IF4 && ST ==> INV2' && ST;
        /*@ // INV2':
          @ assert start < index;
          @ assert (\forall int i; i >= index && i < a.length;
          @                        a[index-1] <= a[i]);
          @ assert sorted ==>
          @        (\forall int i; i >= index && i < a.length; a[i-1] <= a[i]);
          @*/
        // must prove: INV2' && ST ==> (INV2 && ST)[index/index-1];
        index--;
        /*@ // repeat INV2:
          @ assert start <= index;
          @ assert (\forall int i; i > index && i < a.length;
          @                        a[index] <= a[i]);
          @ assert sorted ==>
          @        (\forall int i; i > index && i < a.length; a[i-1] <= a[i]);
          @*/
        /*@ // repeat ST:
          @ assert start >= 0;
          @ assert start < a.length;
          @ assert (\forall int i; i > 0 && i <= start; a[i-1] <= a[i]);
          @*/
      }
      // must prove: INV2 && ST && !COND2 ==> INV1';
      /*@ // INV1':
        @ assert start >= 0;
        @ assert start < a.length;
        @ assert (\forall int i; i > 0 && i <= start; a[i-1] <= a[i]);
        @ assert sorted ==>
        @        (\forall int i; i > 0 && i < a.length; a[i-1] <= a[i]);
        @*/
      // must prove: INV1' ==> INV1[start/start+1]
      start++;
      /*@ // repeat INV1:
        @ assert start >= 0;
        @ assert start <= a.length;
        @ assert (\forall int i; i > 0 && i < start; a[i-1] <= a[i]);
        @ assert sorted ==>
        @        (\forall int i; i > 0 && i < a.length; a[i-1] <= a[i]);
        @*/
    }
    // must prove: INV1 && !COND1 ==> POST;
    /*@ // POST:
      @ assert (\forall int i; i > 0 && i < a.length; a[i-1] <= a[i]);
      @*/
  }


  /**
   * A simple main method for testing.
   * Given a number <I>n</I> of tries on the command line, this program
   * allocates an array of <I>n</I>&nbsp;integers and fills it with random
   * values. It then uses the {@link #sequentialSearch(int[],int)} to
   * search the array for <I>n</I> random numbers, calls {@link
   * #findMaximum(int[])} to determine the maximum number in the array, and
   * calls {@link #bubbleSort(int[])} to sort it.
   */
  /*@
    @ requires args != null;
    @*/
  public static void main(final String[] args)
    throws RuntimeException // redundant but escj prefers to see it ...
  {
    if (args.length != 1) {
      System.err.println
        ("USAGE: jmlrac " + ArrayTests.class.getName() + " <number>");
      return;
    }
    final Random random = new Random();
    final int number = Integer.parseInt(args[0]);
    if (number <= 0) {
      System.err.println("Number of tries must be greater than 0!");
      return;
    }
    final int max = number / 2;
    final int[] a = new int[number];
    for (int i = 0; i < number; i++) {
      a[i] = random.nextInt(max);
    }
    for (int i = 0; i < number; i++) {
      final int item = random.nextInt(number);
      sequentialSearch(a, item);
    }
    findMaximum(a);
    bubbleSort(a);
  }
      
}