/* 
    P/P   *  Method: com.dmdirc.config.prefs.validator.NumericalValidator__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  package com.dmdirc.config.prefs.validator;
    23  
    24  /**
    25   * Validates that a number is within certain bounds.
    26   * 
    27   * @author chris
    28   */
         /* 
    P/P   *  Method: ValidationResponse validate(Object)
          * 
          *  Postconditions:
          *    java.lang.StringBuilder:toString(...)._tainted == 0
          *    return_value == One-of{&new ValidationResponse(validate#1*), &new ValidationResponse(validate#2*), &new ValidationResponse(validate#4*), &new ValidationResponse(validate#6*)}
          *    return_value in Addr_Set{&new ValidationResponse(validate#1*),&new ValidationResponse(validate#2*),&new ValidationResponse(validate#4*),&new ValidationResponse(validate#6*)}
          *    new ValidationResponse(validate#1*) num objects <= 1
          *    new ValidationResponse(validate#1*).failure == &amp;"Must be a valid number"
          *    new ValidationResponse(validate#2*) num objects <= 1
          *    new ValidationResponse(validate#2*).failure == &amp;java.lang.StringBuilder:toString(...)
          *    new ValidationResponse(validate#4*) num objects <= 1
          *    new ValidationResponse(validate#4*).failure == &amp;java.lang.StringBuilder:toString(...)
          *    new ValidationResponse(validate#6*) num objects <= 1
          *    ...
          */
    29  public class NumericalValidator implements Validator<String> {
    30      
    31      /** The minimum value for this number. */
    32      protected final int min;
    33      
    34      /** The maximum value for this number. */
    35      protected final int max;
    36  
    37      /**
    38       * Creates a new numerical validator with the specified bounds.
    39       * 
    40       * @param min The minimum value for the number, or -1 for unlimited.
    41       * @param max The maximum value for the number, or -1 for unlimited.
    42       */
             /* 
    P/P       *  Method: void com.dmdirc.config.prefs.validator.NumericalValidator(int, int)
              * 
              *  Postconditions:
              *    this.max == max
              *    init'ed(this.max)
              *    this.min == min
              *    init'ed(this.min)
              */
    43      public NumericalValidator(int min, int max) {
    44          this.min = min;
    45          this.max = max;
    46      }
    47  
    48      /**
    49       * Retrieves the maximum value that this validator will allow.
    50       * 
    51       * @return This validator's maximum value
    52       */
    53      public int getMax() {
                 /* 
    P/P           *  Method: int getMax()
                  * 
                  *  Postconditions:
                  *    return_value == One-of{231-1, this.max}
                  *    return_value != -1
                  */
    54          return max == -1 ? Integer.MAX_VALUE : max;
    55      }
    56  
    57      /**
    58       * Retrieves the minimum value that this validator will allow.
    59       * 
    60       * @return This validator's minimum value
    61       */    
    62      public int getMin() {
                 /* 
    P/P           *  Method: int getMin()
                  * 
                  *  Postconditions:
                  *    return_value == One-of{-231, this.min}
                  *    return_value != -1
                  */
    63          return min == -1 ? Integer.MIN_VALUE : min;
    64      }
    65      
    66      /** {@inheritDoc} */
    67      @Override
    68      public ValidationResponse validate(final String object) {
    69          int intv;
    70          
    71          try {
                     /* 
    P/P               *  Method: ValidationResponse validate(String)
                      * 
                      *  Postconditions:
                      *    java.lang.StringBuilder:toString(...)._tainted == 0
                      *    return_value in Addr_Set{&amp;new ValidationResponse(validate#2),&amp;new ValidationResponse(validate#4),&amp;new ValidationResponse(validate#6),&amp;new ValidationResponse(validate#1)}
                      *    new ValidationResponse(validate#1) num objects <= 1
                      *    new ValidationResponse(validate#1).failure == &amp;"Must be a valid number"
                      *    new ValidationResponse(validate#2) num objects <= 1
                      *    new ValidationResponse(validate#2).failure == &amp;java.lang.StringBuilder:toString(...)
                      *    new ValidationResponse(validate#4) num objects <= 1
                      *    new ValidationResponse(validate#4).failure == &amp;java.lang.StringBuilder:toString(...)
                      *    new ValidationResponse(validate#6) num objects <= 1
                      *    new ValidationResponse(validate#6).failure == null
                      * 
                      *  Test Vectors:
                      *    this.max: {-1}, {-231..-2, 0..232-2}
                      *    this.min: {-1}, {-231+1..-2, 0..232-1}
                      *    java.lang.Integer:parseInt(...)@72: {-231..-2}, {0..232-1}
                      */
    72              intv = Integer.parseInt(object);
    73          } catch (NumberFormatException ex) {
    74              return new ValidationResponse("Must be a valid number");
    75          }
    76          
    77          if (intv < min && min != -1) {
    78              return new ValidationResponse("Must be at least " + min);
    79          } else if (intv > max && max != -1) {
    80              return new ValidationResponse("Must be at most " + max);
    81          } else {
    82              return new ValidationResponse();
    83          }
    84      }
    85  
    86  }