File Source: ConditionTree.java

         /* 
    P/P   *  Method: com.dmdirc.actions.ConditionTree__static_init
          */
     1  /*
     2   * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
     3   *
     4   * Permission is hereby granted, free of charge, to any person obtaining a copy
     5   * of this software and associated documentation files (the "Software"), to deal
     6   * in the Software without restriction, including without limitation the rights
     7   * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
     8   * copies of the Software, and to permit persons to whom the Software is
     9   * furnished to do so, subject to the following conditions:
    10   *
    11   * The above copyright notice and this permission notice shall be included in
    12   * all copies or substantial portions of the Software.
    13   *
    14   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
    15   * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
    16   * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
    17   * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
    18   * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
    19   * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
    20   * SOFTWARE.
    21   */
    22  
    23  package com.dmdirc.actions;
    24  
    25  import java.util.ArrayDeque;
    26  import java.util.Deque;
    27  
    28  /**
    29   * A condition tree specifies in which order a group of conditions will be
    30   * executed.
    31   *
    32   * @author chris
    33   */
    34  public class ConditionTree {
    35  
    36      /** The possible operations on a condition tree. */
             /* 
    P/P       *  Method: void com.dmdirc.actions.ConditionTree$OPERATION(String, int)
              */
    37      public static enum OPERATION {
    38          /** Only passes if both subtrees are true. */
                 /* 
    P/P           *  Method: com.dmdirc.actions.ConditionTree$OPERATION__static_init
                  * 
                  *  Postconditions:
                  *    $VALUES == &new ConditionTree$OPERATION[](ConditionTree$OPERATION__static_init#6)
                  *    AND == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#1)
                  *    $VALUES[0] == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#1)
                  *    NOOP == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#5)
                  *    $VALUES[4] == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#5)
                  *    NOT == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#4)
                  *    $VALUES[3] == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#4)
                  *    OR == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#2)
                  *    $VALUES[1] == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#2)
                  *    VAR == &new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#3)
                  *    ...
                  */
    39          AND,
    40          /** Passes if either of the subtrees are true. */
    41          OR,
    42          /** Passes if the specified argument is true. */
    43          VAR,
    44          /** Only passes iof the left subtree fails to pass. */
    45          NOT,
    46          /** Doesn't do anything (an empty tree). */
    47          NOOP
    48      }
    49  
    50      /** The left subtree of this tree. */
    51      private ConditionTree leftArg = null;
    52  
    53      /** The right subtree of this tree. */
    54      private ConditionTree rightArg = null;
    55  
    56      /** The argument of this tree (only used for VAR ops). */
    57      private int argument = -1;
    58  
    59      /** The operation that this tree performs. */
    60      private final OPERATION op;
    61  
    62      /**
    63       * Creates a new ConditionTree for a binary operation.
    64       *
    65       * @param op The binary operation to perform
    66       * @param leftArg The left argument/subtree
    67       * @param rightArg The right argument/subtree
    68       */
    69      private ConditionTree(final OPERATION op, final ConditionTree leftArg,
                     /* 
    P/P               *  Method: void com.dmdirc.actions.ConditionTree(ConditionTree$OPERATION, ConditionTree, ConditionTree)
                      * 
                      *  Postconditions:
                      *    this.argument == -1
                      *    this.leftArg == leftArg
                      *    init'ed(this.leftArg)
                      *    this.op == op
                      *    init'ed(this.op)
                      *    this.rightArg == rightArg
                      *    init'ed(this.rightArg)
                      */
    70              final ConditionTree rightArg) {
    71          this.op = op;
    72          this.leftArg = leftArg;
    73          this.rightArg = rightArg;
    74      }
    75  
    76      /**
    77       * Creates a new ConditionTree for a unary operation.
    78       *
    79       * @param op
    80       * @param argument
    81       */
             /* 
    P/P       *  Method: void com.dmdirc.actions.ConditionTree(ConditionTree$OPERATION, ConditionTree)
              * 
              *  Postconditions:
              *    this.argument == -1
              *    this.leftArg == argument
              *    init'ed(this.leftArg)
              *    this.op == op
              *    init'ed(this.op)
              *    this.rightArg == null
              */
    82      private ConditionTree(final OPERATION op, final ConditionTree argument) {
    83          this.op = op;
    84          this.leftArg = argument;
    85      }
    86  
    87      /**
    88       * Creates a new ConditionTree for a VAR operation with the specified
    89       * argument number.
    90       *
    91       * @param argument The number of the argument that's to be tested.
    92       */
             /* 
    P/P       *  Method: void com.dmdirc.actions.ConditionTree(int)
              * 
              *  Postconditions:
              *    this.argument == argument
              *    init'ed(this.argument)
              *    this.leftArg == null
              *    this.rightArg == null
              *    this.op == &com.dmdirc.actions.ConditionTree$OPERATION__static_init.new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#3)
              */
    93      private ConditionTree(final int argument) {
    94          this.op = OPERATION.VAR;
    95          this.argument = argument;
    96      }
    97  
    98      /**
    99       * Creates a new ConditionTree for a NOOP operation.
   100       */
             /* 
    P/P       *  Method: void com.dmdirc.actions.ConditionTree()
              * 
              *  Postconditions:
              *    this.argument == -1
              *    this.leftArg == null
              *    this.rightArg == null
              *    this.op == &com.dmdirc.actions.ConditionTree$OPERATION__static_init.new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#5)
              */
   101      private ConditionTree() {
   102          this.op = OPERATION.NOOP;
   103      }
   104  
   105      /**
   106       * Retrieves the highest argument number that is used in this condition tree.
   107       *
   108       * @return The highest argument number used in this tree
   109       */
   110      public int getMaximumArgument() {
                 /* 
    P/P           *  Method: int getMaximumArgument()
                  * 
                  *  Preconditions:
                  *    (soft) init'ed(this...argument)
                  *    (soft) this...leftArg != null
                  *    (soft) this...rightArg != null
                  *    (soft) init'ed(this.argument)
                  *    (soft) this.leftArg != null
                  *    (soft) this.rightArg != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   111          if (this.op == OPERATION.NOOP) {
   112              return 0;
   113          } else if (this.op == OPERATION.VAR) {
   114              return argument;
   115          } else if (this.op == OPERATION.NOT) {
   116              return leftArg.getMaximumArgument();
   117          } else {
   118              return Math.max(leftArg.getMaximumArgument(), rightArg.getMaximumArgument());
   119          }
   120      }
   121  
   122      /**
   123       * Evaluates this tree with the specified conditions. Returns the result
   124       * of the evaluation.
   125       *
   126       * @param conditions The binary values of each of the conditions used in
   127       * this three
   128       * @return The result of the evaluation of this tree
   129       */
   130      public boolean evaluate(final boolean[] conditions) {
                 /* 
    P/P           *  Method: bool evaluate(bool[])
                  * 
                  *  Preconditions:
                  *    this.op != null
                  *    (soft) init'ed(com.dmdirc.actions.ConditionTree$1__static_init.new int[](ConditionTree$1__static_init#1)[...])
                  *    (soft) conditions != null
                  *    (soft) conditions.length >= 1
                  *    (soft) this.argument < conditions.length
                  *    (soft) init'ed(conditions[...])
                  *    (soft) this...argument >= 0
                  *    (soft) this...leftArg != null
                  *    (soft) this...op != null
                  *    (soft) this...rightArg != null
                  *    ...
                  * 
                  *  Presumptions:
                  *    com.dmdirc.actions.ConditionTree_OPERATION:ordinal(...)@131 in {0..4}
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.actions.ConditionTree$1__static_init.new int[](ConditionTree$1__static_init#1)[...]: {1}, {2}, {3}, {4}, {-231..0, 5..232-1}
                  */
   131          switch (op) {
   132              case VAR:
   133                  return conditions[argument];
   134              case NOT:
   135                  return !leftArg.evaluate(conditions);
   136              case AND:
   137                  return leftArg.evaluate(conditions) && rightArg.evaluate(conditions);
   138              case OR:
   139                  return leftArg.evaluate(conditions) || rightArg.evaluate(conditions);
   140              default:
   141                  return true;
   142          }
   143      }
   144  
   145      /** {@inheritDoc} */
   146      @Override
   147      public boolean equals(final Object obj) {
                 /* 
    P/P           *  Method: bool equals(Object)
                  * 
                  *  Preconditions:
                  *    (soft) init'ed(com.dmdirc.actions.ConditionTree$1__static_init.new int[](ConditionTree$1__static_init#1)[...])
                  *    (soft) init'ed(obj.argument)
                  *    (soft) init'ed(obj.leftArg)
                  *    (soft) obj.op != null
                  *    (soft) init'ed(obj.rightArg)
                  *    (soft) init'ed(this.argument)
                  *    (soft) init'ed(this.leftArg)
                  *    (soft) this.op != null
                  *    (soft) init'ed(this.rightArg)
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   148          return obj instanceof ConditionTree
   149                  && toString().equals(((ConditionTree) obj).toString());
   150      }
   151  
   152      /** {@inheritDoc} */
   153      @Override
   154      public int hashCode() {
                 /* 
    P/P           *  Method: int hashCode()
                  * 
                  *  Preconditions:
                  *    this.op != null
                  *    (soft) init'ed(com.dmdirc.actions.ConditionTree$1__static_init.new int[](ConditionTree$1__static_init#1)[...])
                  *    (soft) init'ed(this.argument)
                  *    (soft) init'ed(this.leftArg)
                  *    (soft) init'ed(this.rightArg)
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   155          return toString().hashCode();
   156      }
   157  
   158      /**
   159       * Retrieves a String representation of this ConditionTree. The string
   160       * representation is a normalised formula describing this tree and all of
   161       * its children. The output of this method will generate an identical tree
   162       * if passed to parseString.
   163       *
   164       * @return A string representation of this tree
   165       */
   166      @Override
   167      public String toString() {
                 /* 
    P/P           *  Method: String toString()
                  * 
                  *  Preconditions:
                  *    this.op != null
                  *    (soft) init'ed(com.dmdirc.actions.ConditionTree$1__static_init.new int[](ConditionTree$1__static_init#1)[...])
                  *    (soft) init'ed(this.argument)
                  *    (soft) init'ed(this.leftArg)
                  *    (soft) init'ed(this.rightArg)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.actions.ConditionTree_OPERATION:ordinal(...)@168 in {0..4}
                  * 
                  *  Postconditions:
                  *    java.lang.String:valueOf(...)._tainted == 0
                  *    init'ed(java.lang.StringBuilder:toString(...)._tainted)
                  *    return_value in Addr_Set{&amp;java.lang.String:valueOf(...),&amp;java.lang.StringBuilder:toString(...),&amp;java.lang.StringBuilder:toString(...),&amp;java.lang.StringBuilder:toString(...),&amp;""}
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.actions.ConditionTree$1__static_init.new int[](ConditionTree$1__static_init#1)[...]: {1}, {2}, {3}, {4}, {-231..0, 5..232-1}
                  */
   168          switch (op) {
   169          case VAR:
   170              return String.valueOf(argument);
   171          case NOT:
   172              return "!" + leftArg;
   173          case AND:
   174              return "(" + leftArg + "&" + rightArg + ")";
   175          case OR:
   176              return "(" + leftArg + "|" + rightArg + ")";
   177          default:
   178              return "";
   179          }
   180      }
   181  
   182      /**
   183       * Parses the specified string into a condition tree.
   184       *
   185       * @param string The string to be parsed
   186       * @return The corresponding condition tree, or null if there was an error
   187       * while parsing the data
   188       */
   189      public static ConditionTree parseString(final String string) {
                 /* 
    P/P           *  Method: ConditionTree parseString(String)
                  * 
                  *  Preconditions:
                  *    string != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  *    new ConditionTree(parseStack#3) num objects <= 1
                  *    new ConditionTree(parseStack#3).argument == -1
                  *    new ConditionTree(parseStack#3).leftArg == null
                  *    new ConditionTree(parseStack#3).op == &amp;com.dmdirc.actions.ConditionTree$OPERATION__static_init.new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#5)
                  *    new ConditionTree(parseStack#3).rightArg == null
                  *    init'ed(new ConditionTree(readTerm#1) num objects)
                  *    new ConditionTree(readTerm#1).argument == 0, if init'ed
                  *    new ConditionTree(readTerm#1).leftArg == null
                  *    new ConditionTree(readTerm#1).op == null
                  *    ...
                  * 
                  *  Test Vectors:
                  *    java.lang.String:charAt(...)@193: {32}, {48..57}, {9}, {10}, {13}, {0..8, 11,12, 14..31, 33..47, 58..216-1}
                  *    java.lang.String:charAt(...)@198: {0..47, 58..216-1}, {48..57}
                  */
   190          final Deque<Object> stack = new ArrayDeque<Object>();
   191  
   192          for (int i = 0; i < string.length(); i++) {
   193              final char m = string.charAt(i);
   194  
   195              if (isInt(m)) {
   196                  final StringBuilder temp = new StringBuilder(String.valueOf(m));
   197  
   198                  while (i + 1 < string.length() && isInt(string.charAt(i + 1))) {
   199                      temp.append(string.charAt(i + 1));
   200                      i++;
   201                  }
   202  
   203                  try {
   204                      stack.add(new ConditionTree(Integer.parseInt(temp.toString())));
   205                  } catch (NumberFormatException ex) {
   206                      return null;
   207                  }
   208              } else if (m != ' ' && m != '\t' && m != '\n' && m != '\r') {
   209                  stack.add(m);
   210              }
   211          }
   212  
   213          return parseStack(stack);
   214      }
   215  
   216      /**
   217       * Parses the specified stack of elements, and returns a corresponding
   218       * ConditionTree.
   219       *
   220       * @param stack The stack to be read.
   221       * @return The corresponding condition tree, or null if there was an error
   222       * while parsing the data.
   223       */
   224      private static ConditionTree parseStack(final Deque<Object> stack) {
                 /* 
    P/P           *  Method: ConditionTree parseStack(Deque)
                  * 
                  *  Preconditions:
                  *    stack != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  *    new ConditionTree(parseStack#3) num objects <= 1
                  *    new ConditionTree(parseStack#3).argument == -1
                  *    new ConditionTree(parseStack#3).leftArg == null
                  *    new ConditionTree(parseStack#3).op == &amp;com.dmdirc.actions.ConditionTree$OPERATION__static_init.new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#5)
                  *    new ConditionTree(parseStack#3).rightArg == null
                  *    init'ed(new ConditionTree(readTerm#1) num objects)
                  *    not_init'ed(new ConditionTree(readTerm#1).argument)
                  *    not_init'ed(new ConditionTree(readTerm#1).leftArg)
                  *    not_init'ed(new ConditionTree(readTerm#1).op)
                  *    ...
                  * 
                  *  Test Vectors:
                  *    java.lang.Character:charValue(...)@230: {0..40, 42..216-1}, {41}
                  *    java.lang.Character:charValue(...)@271: {0..37, 39..216-1}, {38}
                  *    java.lang.Character:charValue(...)@273: {0..123, 125..216-1}, {124}
                  *    java.util.Deque:isEmpty(...)@227: {1}, {0}
                  *    java.util.Deque:isEmpty(...)@243: {1}, {0}
                  *    java.util.Deque:isEmpty(...)@257: {0}, {1}
                  *    java.util.Deque:isEmpty(...)@263: {0}, {1}
                  *    java.util.Deque:size(...)@244: {-231..0, 2..232-1}, {1}
                  */
   225          final Deque<Object> myStack = new ArrayDeque<Object>();
   226  
   227          while (!stack.isEmpty()) {
   228              final Object object = stack.poll();
   229  
   230              if (object instanceof Character && ((Character) object) == ')') {
   231                  final ConditionTree bracket = readBracket(myStack);
   232  
   233                  if (bracket == null) {
   234                      return null;
   235                  } else {
   236                      myStack.add(bracket);
   237                  }
   238              } else {
   239                  myStack.add(object);
   240              }
   241          }
   242  
   243          while (!myStack.isEmpty()) {
   244              if (myStack.size() == 1) {
   245                  final Object first = myStack.pollFirst();
   246                  if (first instanceof ConditionTree) {
   247                      return (ConditionTree) first;
   248                  } else {
   249                      return null;
   250                  }
   251              }
   252  
   253              final ConditionTree first = readTerm(myStack);
   254  
   255              if (first == null) {
   256                  return null;
   257              } else if (myStack.isEmpty()) {
   258                  return first;
   259              }
   260  
   261              final Object second = myStack.pollFirst();
   262  
   263              if (myStack.isEmpty()) {
   264                  return null;
   265              } else {
   266                  final ConditionTree third = readTerm(myStack);
   267  
   268                  if (third != null && second instanceof Character) {
   269                      OPERATION op;
   270  
   271                      if ((Character) second == '&') {
   272                          op = OPERATION.AND;
   273                      } else if ((Character) second == '|') {
   274                          op = OPERATION.OR;
   275                      } else {
   276                          return null;
   277                      }
   278  
   279                      myStack.addFirst(new ConditionTree(op, first, third));
   280                  } else {
   281                      return null;
   282                  }
   283              }
   284          }
   285  
   286          return new ConditionTree();
   287      }
   288  
   289      /**
   290       * Reads and returns a single term from the specified stack.
   291       *
   292       * @param stack The stack to be read
   293       * @return The ConditionTree representing the last element on the stack,
   294       * or null if it was not possible to create one.
   295       */
   296      private static ConditionTree readTerm(final Deque<Object> stack) {
                 /* 
    P/P           *  Method: ConditionTree readTerm(Deque)
                  * 
                  *  Preconditions:
                  *    stack != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  *    new ConditionTree(readTerm#1) num objects <= 1
                  *    new ConditionTree(readTerm#1).argument == -1
                  *    init'ed(new ConditionTree(readTerm#1).leftArg)
                  *    new ConditionTree(readTerm#1).op == &amp;com.dmdirc.actions.ConditionTree$OPERATION__static_init.new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#4)
                  *    new ConditionTree(readTerm#1).rightArg == null
                  *    new ConditionTree(readTerm#1*) num objects <= 1
                  *    not_init'ed(new ConditionTree(readTerm#1*).argument)
                  *    not_init'ed(new ConditionTree(readTerm#1*).leftArg)
                  *    not_init'ed(new ConditionTree(readTerm#1*).op)
                  *    ...
                  * 
                  *  Test Vectors:
                  *    java.lang.Character:charValue(...)@299: {0..32, 34..216-1}, {33}
                  *    java.util.Deque:isEmpty(...)@300: {0}, {1}
                  */
   297          final Object first = stack.pollFirst();
   298  
   299          if (first instanceof Character && (Character) first == '!') {
   300              if (stack.isEmpty()) {
   301                  return null;
   302              }
   303  
   304              return new ConditionTree(OPERATION.NOT, readTerm(stack));
   305          } else {
   306              if (!(first instanceof ConditionTree)) {
   307                  return null;
   308              }
   309  
   310              return (ConditionTree) first;
   311          }
   312      }
   313  
   314      /**
   315       * Pops elements off of the end of the specified stack until an opening
   316       * bracket is reached, and then returns the parsed content of the bracket.
   317       *
   318       * @param stack The stack to be read for the bracket
   319       * @return The parsed contents of the bracket, or null if the brackets were
   320       * mismatched.
   321       */
   322      private static ConditionTree readBracket(final Deque<Object> stack) {
                 /* 
    P/P           *  Method: ConditionTree readBracket(Deque)
                  * 
                  *  Preconditions:
                  *    (soft) stack != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  *    new ConditionTree(parseStack#3) num objects <= 1
                  *    new ConditionTree(parseStack#3).argument == -1
                  *    new ConditionTree(parseStack#3).leftArg == null
                  *    new ConditionTree(parseStack#3).op == &amp;com.dmdirc.actions.ConditionTree$OPERATION__static_init.new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#5)
                  *    new ConditionTree(parseStack#3).rightArg == null
                  *    init'ed(new ConditionTree(readTerm#1) num objects)
                  *    new ConditionTree(readTerm#1).argument == 0, if init'ed
                  *    new ConditionTree(readTerm#1).leftArg == null
                  *    new ConditionTree(readTerm#1).op == null
                  *    ...
                  * 
                  *  Test Vectors:
                  *    java.lang.Character:charValue(...)@329: {0..39, 41..216-1}, {40}
                  *    java.util.Deque:isEmpty(...)@326: {1}, {0}
                  */
   323          final Deque<Object> tempStack = new ArrayDeque<Object>();
   324          boolean found = false;
   325  
   326          while (!found && !stack.isEmpty()) {
   327              final Object object = stack.pollLast();
   328  
   329              if (object instanceof Character && ((Character) object) == '(') {
   330                  found = true;
   331              } else {
   332                  tempStack.addFirst(object);
   333              }
   334          }
   335  
   336          if (found) {
   337              return parseStack(tempStack);
   338          } else {
   339              return null;
   340          }
   341      }
   342  
   343      /**
   344       * Determines if the specified character represents a single digit.
   345       *
   346       * @param target The character to be tested
   347       * @return True if the character is a digit, false otherwise
   348       */
   349      private static boolean isInt(final char target) {
                 /* 
    P/P           *  Method: bool isInt(char)
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   350          return target >= '0' && target <= '9';
   351      }
   352  
   353      /**
   354       * Creates a condition tree by disjoining the specified number of arguments
   355       * together.
   356       *
   357       * @param numArgs The number of arguments to be disjoined
   358       * @return The corresponding condition tree
   359       */
   360      public static ConditionTree createDisjunction(final int numArgs) {
                 /* 
    P/P           *  Method: ConditionTree createDisjunction(int)
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  *    new ConditionTree(parseStack#3) num objects <= 1
                  *    new ConditionTree(parseStack#3).argument == -1
                  *    new ConditionTree(parseStack#3).leftArg == null
                  *    new ConditionTree(parseStack#3).op == &amp;com.dmdirc.actions.ConditionTree$OPERATION__static_init.new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#5)
                  *    new ConditionTree(parseStack#3).rightArg == null
                  *    init'ed(new ConditionTree(readTerm#1) num objects)
                  *    new ConditionTree(readTerm#1).argument == 0, if init'ed
                  *    new ConditionTree(readTerm#1).leftArg == null
                  *    new ConditionTree(readTerm#1).op == null
                  *    ...
                  * 
                  *  Test Vectors:
                  *    java.lang.StringBuilder:length(...)@364: {0}, {-231..-1, 1..232-1}
                  */
   361          final StringBuilder builder = new StringBuilder();
   362  
   363          for (int i = 0; i < numArgs; i++) {
   364              if (builder.length() != 0) {
   365                  builder.append('|');
   366              }
   367  
   368              builder.append(i);
   369          }
   370  
   371          return parseString(builder.toString());
   372      }
   373  
   374      /**
   375       * Creates a condition tree by conjoining the specified number of arguments
   376       * together.
   377       *
   378       * @param numArgs The number of arguments to be conjoined
   379       * @return The corresponding condition tree
   380       */
   381      public static ConditionTree createConjunction(final int numArgs) {
                 /* 
    P/P           *  Method: ConditionTree createConjunction(int)
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  *    new ConditionTree(parseStack#3) num objects <= 1
                  *    new ConditionTree(parseStack#3).argument == -1
                  *    new ConditionTree(parseStack#3).leftArg == null
                  *    new ConditionTree(parseStack#3).op == &amp;com.dmdirc.actions.ConditionTree$OPERATION__static_init.new ConditionTree$OPERATION(ConditionTree$OPERATION__static_init#5)
                  *    new ConditionTree(parseStack#3).rightArg == null
                  *    init'ed(new ConditionTree(readTerm#1) num objects)
                  *    new ConditionTree(readTerm#1).argument == 0, if init'ed
                  *    new ConditionTree(readTerm#1).leftArg == null
                  *    new ConditionTree(readTerm#1).op == null
                  *    ...
                  * 
                  *  Test Vectors:
                  *    java.lang.StringBuilder:length(...)@385: {0}, {-231..-1, 1..232-1}
                  */
   382          final StringBuilder builder = new StringBuilder();
   383  
   384          for (int i = 0; i < numArgs; i++) {
   385              if (builder.length() != 0) {
   386                  builder.append('&');
   387              }
   388  
   389              builder.append(i);
   390          }
   391  
   392          return parseString(builder.toString());
   393      }
   394  
   395  }








SofCheck Inspector Build Version : 2.17854
ConditionTree.java 2009-Jun-25 01:54:24
ConditionTree.class 2009-Sep-02 17:04:13
ConditionTree$1.class 2009-Sep-02 17:04:13
ConditionTree$OPERATION.class 2009-Sep-02 17:04:13