Skip to main content
CSE 331: Software Design & Implementation

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 final resulting assertion, but do not weaken it (such as dropping facts that are useful). Separate any simplified statement from the original by “\(\leftrightarrow\)”.

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

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

    // INVERTIBLE OPERATIONS VERSION
{{ 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 }}

// SUBSCRIPTS VERSION
{{ y > 5 and z > 2 }}
x = 4 * y - 3;
{{ y > 5 and z > 2 and x = 4y - 3 }}
y = y - 5;
{{ y_0 > 5 and z > 2 and x = 4y_0 - 3 and y = y_0 - 5 }}
z = z * y;
{{ P: y_0 > 5 and z_0 > 2 and x = 4y_0 - 3 and y = y_0 - 5 and z = z_0 * y}}
{{ 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. Use subscripts or invertible operations.

    // 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;
}

    // INVERTIBLE OPERATIONS VERSION
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;
}

// SUBSCRIPTS VERSION
public static int nextSquare(int x) {
  int y = x * x;
  {{ y = x^2 }}
  y = y + (2 * x);
  {{ y_0 = x^2 and y = y_0 + 2x }}
  y = y + 1;
  {{ P: y_0 = x^2 and y_1 = y_0 + 2x and y = y_1 + 1 }} <--> {{ 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;
    {{ _________________________ }}
    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 }}
    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;

Task 4 — Everybody Loops

In this problem, we will show the correctness of a method containing a loop that finds the quotient of \(x\) divided by 10, i.e., the largest value \(y\) such that \(10y \le x\). To say that \(y\) is the largest such value means that any larger value would not satisfy the inequality, i.e., that \(10(y+1) \not\le x\).

We denote the initial value of the parameter \(x\) at the top of the method by \(x_0\). This is explicitly stated in the precondition as the fact “\(x = x_0\)” (note this is not strictly necessary - you always know \(x = x_0\) until you modify it!). The first two facts of Q are from the spec postcondition, which say that \(y\) is the quotient of \(x_0\) divided by 10. The third fact is specific to our implementation, and says that \(x\) is the remainder, i.e., the remaining amount not divisible by 10.

This method calculates the quotient without division. Instead, it just uses subtraction. It operates by increasing y and decreasing x each time around. The first part of the invariant says that the distance from \(x_0\) down to \(10y\) (i.e., \(x_0 - 10y\)) is the same as the distance from \(x\) down to 0 (i.e., \(x - 0 = x\)). The second part of the invariant says that \(x\) has not moved below 0 (i.e., \(x \ge 0\)).

Use subscripts only.

// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
  {{ x = x_0 and x_0 >= 0 }}
  int y = 0;
  {{ P1: _________________________ }}
  {{ Inv: x_0 - 10y = x and x >= 0 }}
  while (x >= 10) {
    {{ _________________________ }}
    y = y + 1;
    {{ _________________________ }}
    x = x - 10;
    {{ P3: _________________________ }}
    {{ Q2: _________________________ }}
  }
  {{ P2: _________________________ }}
  {{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
  return y;
}

  1. Check (1): Fill in P1, then show that the invariant is true when we get to the top of the loop the first time.

    P1 is \(x = x_0\), \(x_0 \ge 0\), and \(y = 0\).

    Math: The first part of the invariant holds because

    \[ \begin{aligned} x_0 - 10y &= x - 10y && \text{since } x = x_0 \\ &= x && \text{since } y = 0. \end{aligned} \]

    Math: The second part holds because \(x = x_0 \ge 0\).

    English, first part of the invariant: We know \(x = x_0\) and \(y = 0\). So \(x_0 - 10y = x\).

    English, second part of the invariant: We know \(x = x_0\) and \(x_0 \ge 0\), so \(x \ge 0\).

  2. Check (3): Fill in P2, then show that Q1 holds when we exit the loop.

    When we exit the loop, P2 tells us that the invariant holds and \(x < 10\).

    Math: For the first part of Q1,

    \[ \begin{aligned} 10y &= x_0 - x && \text{since } x_0 - 10y = x \\ &\le x_0 && \text{since } x \ge 0, \end{aligned} \]

    Math: For the second part of Q1,

    \[ \begin{aligned} x_0 &= x + 10y && \text{since } x_0 - 10y = x \\ &< 10 + 10y && \text{since } x < 10 \\ &= 10(y + 1). \end{aligned} \]

    Math: The third part of Q1, \(x = x_0 - 10y\), is a restatement of the first part of the invariant.

    Since the method returns \(y\), these facts establish the required bounds for the quotient.

    English, first part of Q1: From \(x_0 - 10y = x\), we get \(x_0 = x + 10y\). Since \(x \ge 0\), \(10y \le x_0\).

    English, second part of Q1: Again, \(x_0 = x + 10y\). Since \(x < 10\), we get \(x_0 < 10 + 10y = 10(y+1)\).

    English, third part of Q1: This is exactly the first invariant fact. Since the method returns \(y\), this proves the required quotient bounds.

  3. Check (2): Fill in Q2 (Hint: what do we know at the end of a loop?). Then, forward reason to P3. Show that P3 implies Q2, proving that the body of the loop is correct.

    {{ Inv: x_0 - 10y = x and x >= 0 }}
while (x >= 10) {
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y_0) = x and x >= 0 and x >= 10 and y = y_0 + 1 }}
x = x - 10;
{{ P3: x_0 - 10(y_0) = x_1 and x_1 >= 0 and x_1 >= 10 and
   y = y_0 + 1 and x = x_1 - 10
 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
}

    Math: For the first part of the invariant, P3 gives

    \[ \begin{aligned} x &= x_1 - 10 && \text{since } x = x_1 - 10 \\ &= x_0 - 10y_0 - 10 && \text{since } x_1 = x_0 - 10y_0 \\ &= x_0 - 10(y_0 + 1) && \text{algebra} \\ &= x_0 - 10y && \text{since } y = y_0 + 1. \end{aligned} \]

    Math: For the second part, P3 gives \(x_1 \ge 10\) and \(x = x_1 - 10\). Therefore,

    \[ x = x_1 - 10 \ge 10 - 10 = 0. \]

    English, first part of the invariant: The algebra shows that after the loop body, \(x_0 - 10y = x\) still holds.

    English, second part of the invariant: The old value is \(x_1 \ge 10\), and the new value is \(x = x_1 - 10\), so \(x \ge 0\).