Assignment 3: Verification Condition Generation

The goal of this simple assignment is for you to solve Exercise 5.3 on page 151 in your textbooks using Z3. Based on the concept of weakest preconditions that we learned today, encode the given basic paths as Z3 formulas manually using pen-and-paper. The textbook requires that you establish validity in both the theory of integers and theory of rationals. For the purpose of this assignment, establish validity in both the theory of integers and theory of reals (instead of rationals). Each basic path should correspond to one Z3 assertion in the theory of integers and one in the theory of rationals.

You can leverage rise4fun for this assignment: http://rise4fun.com/Z3 Links to an external site.

Your solution should be a text entry containing the encoded verification conditions as Z3 constraints. Leave comments in the entry so that I know which sections belong to which VCs.