Chapter 4 Questions.

Program Verification.

Semantics of programs: the partial correctness relation par.

Recall what parphi P psi means: "For all stores that satisfy phi, if P runs on such a store and if that run terminates, then the resulting store satisfies psi."

Question 1

Which of the following triples is valid with respect to the partial correctness relation par?
(As in the textbook, we assume all occurring variables x, y, ... have type integer.)
  1. x > -1 y = x + x; x > -2
  2. x = 5 y = 3 x = y; y = x; x = 3 y = 5
  3. T while (x > 4) x = x - 1; x = 4
  4. T if (x > 5) { y = x - 1;} else {y = x + 1;} y > 3
  5. T x = 1; x = 2; x = 1 x = 2

Question 2

Which of the following programs P satisfies the triple T P z = max(x,y) with respect to partial correctness: parT P z = max(x,y)
where max(x,y) is the larger number of x and y (e.g. max(-1,3) = 3)?

  1. if (x > y) {
      z = x + 1;
} else {
      z = y + 1;
}
z = z - 1;

  2. if (x > y) {
      z = y + 1;
} else {
      z = x + 1;
} 
z = z - 1;

  3. if (x > y) {
      z = x;
} else {
      z = y + 1;
}
z = z - 1;

  4. if (x > y) {
      z = x + 1;
} else {
      z = y + 1;
}
z = z + 1;

  5. if (x > y) {
      z = y;
} else {
      z = x;
}
z = z;

Question 3

The program P:
x = y;
if (x < z) { x = z; }

satisfies which of the following Hoare triples with respect to the partial correctness relation par?
  1. x = y P x = y
  2. x < y P x = y
  3. y < z P x = z
  4. y = z P x < y
  5. None of the above.

Question 4

Consider the program:
y = x - y - 1;
x = x + 1;
y = 2*x + y;

What fact about the starting state would guarantee that, after the program has run, x = y?
  1. x = y.
  2. y = -1.
  3. y = 2x.
  4. y = y + 3.
  5. None of the above.

Invariants of while-statements.

Question 5

Which of the following is an invariant of the while-statement in the program

a = 0;
z = 0;
while (a != y)
{
      z = z + x;
      a = a + 1;
}
with respect to partial correctness par ?
  1. z = x * y
  2. z = x * a
  3. z = a * y
  4. y = z * a
  5. x = y * a

Question 6

Which of the following is an invariant of the while-statement in the program
z = 0;
a = 1;
while (a != y+1) {
	z = z + a;
	a = a + 1;
}
with respect to partial correctness par ?
  1. z = a + y.
  2. z = a(a + y).
  3. 2z = (a - 1)a.
  4. 2z = a + 1.
  5. The while loop has no invariant.
Back to chapter index.