CSE 331: Section 3 — Reasoning (Solutions)

Task 1 — Found Guilty of Reason

In this problem, you will practice proving correctness of straight-line code using forward reasoning.

Fill in each blank by applying the rules exactly as taught in lecture. Then, if you want, you can simplify the resulting assertion, but do not weaken it (such as substituting/dropping facts). Separate any simplified statement from the original by “\(\leftrightarrow\)”.

1. Use forward reasoning to fill in the missing assertions in the following code:

   {{ y > 5 and z > 2 }}
   x = 4 * y - 3;
   {{ _________________________ }}
   y = y - 5;
   {{ _________________________ }}
   z = z * y;
   {{ P: ______________________ }}
   {{ Q: x < 2z + 20 }}
   

   {{ y > 5 and z > 2 }}
   x = 4 * y - 3;
   {{ y > 5 and z > 2 and x = 4y - 3 }}
   y = y - 5;
   {{ y + 5 > 5 and z > 2 and x = 4(y + 5) - 3 }}
   z = z * y;
   {{ P: y + 5 > 5 and z / y > 2 and x = 4(y + 5) - 3 }}
   {{ Q: x < 2z + 20 }}
   

2. First, fill in Q using the postcondition (hint, how does y relate to the @returns clause?). Then, use forward reasoning to fill in the missing assertions in the following code:

   // Computes the square of (x + 1)
   // @param x The number to increment and square
   // @return (x + 1)^2
   public static int nextSquare(int x) {
     int y = x * x;
     {{ _________________________ }}
     y = y + (2 * x);
     {{ _________________________ }}
     y = y + 1;
     {{ P: ______________________ }}
     {{ Q: ______________________ }}
     return y;
   }
   

   public static int nextSquare(int x) {
     int y = x * x;
     {{ y = x^2 }}
     y = y + (2 * x);
     {{ y - 2x = x^2 }}
     y = y + 1;
     {{ P: y - 2x - 1 = x^2 }}  <-->  {{ y = x^2 + 2x + 1 }}
     {{ Q: y = (x + 1)^2 }}
     return y;
   }
   

Task 2 — Does a Duck Say “Back”?

In this problem, you will practice proving correctness of straight-line code using backward reasoning.

1. Use backward reasoning to fill in the missing assertions in the following code:

   {{ P: x < w + 1 and w > 0 }}
   {{ Q: ______________________ }}
   y = 4 * w;
   {{ _________________________ }}
   x = x * 2;
   {{ _________________________ }}
   z = x - 8;
   {{ z < y }}
   

   {{ P: x < w + 1 and w > 0 }}
   {{ Q: 2x - 8 < 4w }}  <-->  {{ 2x < 4w + 8 }}  <-->  {{ x < 2w + 4 }}
   y = 4 * w;
   {{ 2x - 8 < y }}
   x = x * 2;
   {{ x - 8 < y }}
   z = x - 8;
   {{ z < y }}
   

2. Use backward reasoning to fill in the missing assertions in the following code snippet:

       {{ Q: ______________________ }}
       int b = 2 * c;
       {{ _________________________ }}
       int c = c - 1;
       {{ _________________________ }}
       int a = b + 1;
       {{ a >= c }}
       return a;
   

       {{ Q: 2c + 1 >= c - 1 }}  <-->  {{ c >= -2 }}
       int b = 2 * c;
       {{ b + 1 >= c - 1 }}
       int c = c - 1;
       {{ b + 1 >= c }}
       int a = b + 1;
       {{ a >= c }}
       return a;
   

Task 3 — Nothing To Be If-ed At

Use forward reasoning to fill in the assertions.

  {{ 0 <= s < len and d >= 0 }}
  int w;
  if (s + d <= len) {
    {{ ___________________________________ }}
    w = d;
    {{ P1: ________________________________ }}
  } else {
    {{ ___________________________________ }}
    w = len - s;
    {{ P2: ________________________________ }}
  }
    {{ _________________________ }}
  return w;

  {{ 0 <= s < len and d >= 0 }}
  int w;
  if (s + d <= len) {
    {{ 0 <= s < len and d >= 0 and s + d <= len }}
    w = d;
    {{ P1: 0 <= s < len and d >= 0 and s + d <= len and w = d }}
  } else {
    {{ 0 <= s < len and d >= 0 and s + d > len }}
    w = len - s;
    {{ P2: 0 <= s < len and d >= 0 and s + d > len and w = len - s }}
  }
    {{ P1 or P2 }}
  return w;