/****************************************************************************** Copyright (c) Gunnar Gotshalks. All Rights Reserved. Permission to use, copy, modify, and distribute this software and its documentation for NON-COMMERCIAL purposes and without fee is hereby granted. *******************************************************************************/ /** Define objects that represent polynomial terms.

@author Gunnar Gotshalks @version 1.0 2008 June 10 */ import java.util.*; public class Term { /******************************************************************************* The ADT fields *******************************************************************************/ /** A dummy variable to get the class invariant into javadoc documentation; see field detail. 

null_list_zero_term: coefficient = 0 implies variables.is_empty
sorted_variables: forall j, k : 1 .. #variables | j < k
                      :: variables[j] < variables[k]
unique_variables: forall j, k : 1 .. #variables | j ~= k
                      :: variables[j].name ~= variables[k].name
*/ protected boolean class_invariant; /** The coefficient for the term. The coefficient is not public as it cannot be changed independently of the variables, due to the class invariant that a zero coefficient implies no variables. */ protected int coefficient; /** The list of the variables in the term. The variables have unique names and are sorted in UNI-CODE order from low to high -- the normal lexicographic ordering. The field would normally be private as only the insert operation should be able to modify the list of variables. However the test classes need to access the list to check out its contents. */ protected LinkedList variables; /******************************************************************************* The constructor *******************************************************************************/ /** Create a term with zero coefficient 
Require True
Ensure zero_coefficient_term : coefficient = 0 and variables.is_empty
*/

public Term () {
  coefficient = 0;
  variables = new LinkedList  ();
}

/******************************************************************************
Read operations
*******************************************************************************/
/** Return the coefficient for the term.
 
 Require True
 Ensure Result = coefficient
 

 */

public int get_coefficient() { return coefficient; }

/******************************************************************************
Write operations
*******************************************************************************/
/** Change the coefficient for the term.
 
 Require True
 Ensure coefficient = new_coefficient
          new_coefficient = 0  implies  variables.is_empty
 

 */

public void set_coefficient(int new_coefficient) {
  coefficient = new_coefficient;
  if (new_coefficient == 0) { variables = new LinkedList  (); }
}

/** Insert the new variable into the correct position in the list.

Require not_in_term: not in_term(new_variable)
        not_zero_coefficient: coefficient ~= 0
Ensure
  in_term: new_variable in variables
  old_variables_still_there: forall v in old variables :: v in variables
  one_more_variable: variables.count = old variables.count + 1
  coefficient_unchanged: coefficient = old coefficient


*/

public void insert(Variable new_variable) {
  Variable term_variable;
  int index;                  // Keep track of where to insert the new variable
  if (variables.isEmpty()) {  // First variable can be simply added to the list
    variables.add(new_variable.deep_clone());
  }

// The new variable must be inserted into the correct position within an
// existing list of variables.  Prime the search by getting the first
// variable in the list.

  else {
    ListIterator list_iter = variables.listIterator(0);
    term_variable = list_iter.next();
    index = 0;

// Search for the insertion point for the new variable
// Invariant: forall k : 0...index - 1
//                :: variables[k].name < new_variable.name

    while (  new_variable.name.compareTo(term_variable.name) > 0
          && list_iter.hasNext()) {
      term_variable = (Variable) list_iter.next();
      index++;
    }

// The variable is inserted at the index location if there is at least one
// variable with a name later in the sort sequence than the name of the new
// variable.  Otherwise the new variable is added at the end of the list.

    if (new_variable.name.compareTo(term_variable.name) < 0) {
       variables.add(index, new_variable.deep_clone()); }
    else { variables.add(new_variable.deep_clone());  }
  }
}

/******************************************************************************
Comparison Operations
*******************************************************************************/
/** Is this term greater than the other term; depends only upon the variables
not the value.

Require  other_term ~= null
Ensure   Result <--> 
  (exists index : 0..min(#this_term.variables, #other_term.variables)
    :: (this_term.variables[index] > other_term_variables[index]
    and forall j : 0..index-1
           :: this_term.variables[index] = other_term_variables[index]))
  or
  ( (forall index : 0..min(#this_term.variables, #other_term.variables)
    :: this_term.variables[index] =other_term_variables[index] )
  and (#this_term.variables > #other_term.variables) )


*/

public boolean greater_than(Term other_term) {
// Not determined becomes false if a greater than relationship holds between
// a pair of corresponding variables both variable lists.
  boolean not_determined = true;
  boolean Result = false;        // Arbitrary value to avoid warning message
  Variable this_variable, other_variable;
  
  ListIterator this_term_iter = variables.listIterator(0);
  ListIterator other_term_iter = other_term.variables.listIterator(0);

//Invariant: forall k : 0 .. index - 1 :: this_variable = other_variable

  while (this_term_iter.hasNext() && other_term_iter.hasNext()
         && not_determined) {
    this_variable = (Variable) this_term_iter.next();
    other_variable = (Variable) other_term_iter.next();
    if (this_variable.less_than(other_variable)) {
      Result = false; not_determined = false; }
    else {
      if (other_variable.less_than(this_variable)) {
        Result = true; not_determined = false; }
    }
  }

// If greater than has not been determined by comparing all the variables in the
// shorter list, then greater than depends upon which list of variables is
// shorter.

  if (not_determined) {
    Result = this_term_iter.hasNext() && !other_term_iter.hasNext(); }
  return Result;
}

/** Is this term equal to the other term; depends only upon the variables not
the value.

Require  other_term ~= null
Ensure  Result <--> 
        forall j : 0..#this_term.variables-1
             :: this_term.variables[index] = other_term_variables[index])
    and #this_term.variables = #other_term.variables) )


*/

public boolean equals (Term other_term) {
  boolean Result = true;      // True if no variables
  Variable this_variable, other_variable;
  
  ListIterator this_term_iter = variables.listIterator(0);
  ListIterator  other_term_iter = other_term.variables.listIterator(0);

// Invariant: forall k : 0 .. index - 1 :: this_variable = other_variable

  while (Result && this_term_iter.hasNext() && other_term_iter.hasNext()) {
    this_variable = (Variable) this_term_iter.next();
    other_variable = (Variable) other_term_iter.next();
    Result = this_variable.equals(other_variable);
  }
  
  return Result && !this_term_iter.hasNext() && !other_term_iter.hasNext();

}

/******************************************************************************
Conversion Operations
*******************************************************************************/
/** Return the string representation of the term.

Require True
Ensure  Result = (+,-) coefficient
               + forall v in variables :: "(" + (toString(v)) +")"


*/

public String toString () {
  String Result;
  if (coefficient >= 0) { Result = "+" + coefficient; }
  else { Result = "" + coefficient; }
  ListIterator var_iter = variables.listIterator(0);

// Invariant: forall k : 0..index-1 :: string_rep(variables[k]) in Result

  while (var_iter.hasNext()) {
    Result = Result + "(" + var_iter.next().toString() + ")";
  }
  return Result;
}

/*******************************************************************************
Clone operators
*******************************************************************************/
/** Create a copy of all levels of the term.

Require True
Ensure Result is an independent copy of this term


*/

public Term deep_clone () {
  Term Result;                // The cloned term
  Result = new Term();
  Result.set_coefficient(coefficient);

// Copy each variable in variables to the Result variables.
// Because the list iterator processes the variables in list sequence, the
// copied variables can be added to the end of the result list of variables.

  Variable var_old, var_new;
  ListIterator variable_iter = variables.listIterator(0);

// Invariant: forall index : 0 .. index_of(var_old) - 1
//                :: Result.variables[index] = variables[index]

  while (variable_iter.hasNext()) {
    var_old = (Variable) variable_iter.next();
    var_new = new Variable(var_old.name, var_old.exponent);
    Result.variables.add(var_new);
  }

  return Result;
}

/*******************************************************************************
Support debug procedures
*******************************************************************************/

/** Print the String on the current output line, then start a new output line 
 and go to a new line.  Hides the call to System.out */
@SuppressWarnings("unused")
private static void println(String item) { System.out.println(item); }

/** Print the String on current output line.  Hides the call to System.out */
@SuppressWarnings("unused")
private static void print(String item) { System.out.print(item); }

}