Index
Blog

# 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