• Practice deriving pre and post-conditions.
• Practice identifying invariants in a loop.
• Think about how to test code you write.

Your TA will introduce assertions and discuss:

• Create a R20 project.
• Create a R20 class with a main method.
• Paste the following code into your R20 class (not in main method):

  // #1
  // Precondition: -10 <= x <= 7  
  // Postcondition: ?
  // QUESTION: What is the postcondition?
  public static int funcOne(int x) {
  
      // Enforce specified precondition in method
      assert (x >= -10 && x <= 7);
      return (3 * x * x * x) - (2 * x * x) + 5;
  }
  
  // #2
  // Preconditions: -5 <= x <= -2, 6 <= y <= 13   
  // Postcondition: ?
  // QUESTION: What is the postcondition?
  public static int funcTwo(int x, int y) {
  
      // Enforce specified precondition in method
      assert (x >= -5 && x <= -2);
      assert (y >= 6  && y <= 13);
      return (3 * x * x * x) - (y * x * x) + 11;
  }
  
  // #3
  // Precondition: ?
  // Postcondition: 0.25 <= return value <= 1.0
  // QUESTION: What is the precondition?
  public static double funcThree(double x) {
  
      return 1.0 / x; 
  }
  
  
  // #4
  // Precondition: x is an integer  
  // Postcondition: returns an even integer
  // QUESTION: Is the postcondition true? Why or why not?
  public static int funcFour(int x) {
  
      int retVal;
      if (x % 2 == 0) {
          retVal = x * x - x;
      } else {
          retVal = (x + x) * (x + x);
      }
      assert(retVal % 2 == 0);
      return retVal;
  }
  
  // #5
  // Precondition: x >= 1
  // QUESTION: Find the loop invariants before, during, and after the loop.
  public static void funcFive(int x) {
  
      int result = 1;
      int i = 0;
      do {
          i++;
          result = result * i;
      } while (i < x);
  }
  
  // #6
  // QUESTION: Does this correct swap the locals a and b? Why or why not?
  public static void funcSix(int a, int b) {
  
      System.out.println("Before: a = " + a + " and b = " + b);
      if (a < b) {
          int r = a % b;
          a = b;
          b = r;
      }
      else {
          int r = b;
          b = a;
          a = r;
      }
      System.out.println("After: a = " + a + " and b = " + b);
  }
  

THE GOAL of this recitation is to improve you as programmers by developing the ability to test code so you can find errors and be more confident that it works as intended. We can do this writing some useful test code and/or by applying some of the mathematical reasoning skills we've developed over the semester.

• The code we provided has 6 methods.
• Each method has comments that ask a question.
• Questions 1 and 2 give you preconditions and ask you find the postcondition.
• Think about adding code to main to test the functions for the range specified in the precondition.
• Question 3 gives you a postcondition and asks you to find a precondition.
• Step One: Think about adding code to main method to try a large range of parameter values.
• Step Two: Narrow down your range to establish what the precondition is.
• Question 4 asks you to verify a postcondition.
• Figure out what the code is doing, then use logical reasoning to verify.
• Question 5 asks you to find the loop invariants.
• You can get the information you adding prints to the function code or by using the debugger.
• Question 6 asks you to verify that a swap occurs.
• Figure out what the code is doing, then use logical reasoning to verify.