CIS 301. Preview of Exam #3.

• Consider the CTL model of four states on the black board. Explain in detail why, or why not, the four relationships (a) to (d) below hold, for the indicated states:
  • (a) s0 |== p --> !q
  • (b) s1 |== AX(EX p)
  • (c) s3 |== EF (!p & q)
  • (d) s1 |== EG (p --> AF q).

• Consider the CTL formula given by
  

  EG (!p --> AG (q | AF r)).
  

  where the events p, q, and r are

  • p : Anonymizer of source is enabled
  • q : Target accepts call
  • r : Caller-id of target is active.

  Translate the formula above into plain English.

• Prove the partial correctness (| phi |) P (| x = 2 + y |) for the program P given below:

    x = 2 * x - y;
    if (x < y) {
       x = -x + y;
    } else {
       y = x + y;
    }
    x = y + x;
  

  For which phi can you prove this? (Your phi should be such that it is implied by any other such formula.)

• Let x be any integer and y any natural number 0,1,2,... Given

  x**0  = 1
  x**(y+1) = (x**y) * x
  

  prove partial correctness of (| T |) Expo (| z = x**y |) for the program Expo given below:

    z = 1;
    a = 0;
    while (a != y) {
      z = z * x;
      a = a + 1;
    }
  

• For which values of a, x, y, and z does the program Expo terminate? (Explain why.)