Homework 3.

Consider the algorithms 5 and 6 at page 70 of the lecture notes. Algorithm 5 searches forward from the initial condition, trying to determine whether a state violating the invariant can be reached. Algorithm 6 searches backwards from the complement of the invariant, trying to determine whether the initial condition can be reached.

Obviously, it is possible to combine these algorithms and write an algorithm that searches at the same time forwards from the initial condition, and backwards from the complement of the invariant, stopping as soon as the searches terminate, or meet at a common state. Write such an algorithm, paying attention to stopping as soon as you can determine that no path from the initial condition to the complement of the invariant exists. Notice that your algorithm can use the Pre and Post operators presented in class.