Midterm Exam

Midterm

Date: 9 April - 16 April

1. Define reaching definitions for a post-test UNTIL loop of the following form: (10pts)

Y := X;
Z := 1;
DO
  Z := Z * Y;
  Y := Y - 1;
UNTIL Y = 0;
SKIP;

This loop is exactly like a while except the body executes once before the condition is checked. Don’t worry about what the loop does, just label statements and define reaching definitions for each label. What I want to see are the RD entry and exit definitions for each labeled term.

1. Define a general procedure for defining reaching definitions for any UNTIL loop. (10pts)

2. Thinking about the UNTIL loop again, is the statement X is not modified a safety condition? Please explain why or why not. (5pts)

3. Thinking about the UNTIL loop again, is the statement Y is modified a liveness condition? Please explain why or why not. (5pts)

4. Thinking about they UNTIL loop again, is the statement Y does not increase an invariant? Please explain why or why not. (5pts)

5. Answer the following questions by indicating if they are satisfiable and/or valid: (2pts each)

   1. A ∧ B ∨ ~(A ∧ B)
   2. A ∧ ~A
   3. A ∧ B ∧ ~(A ∧ B)
   4. A ∧ B ∧ C
   5. A => ~A