Assignment 3

Submission Instructions This assignment is due at 5pm on the date indicated in the class calendar. See the note at the end of this document for instructions on how to submit your code.

Collaboration: You are allowed to collaborate with one other person for this assignment, but each of you is responsible for submitting your own solution. If you do collaborate with someone else, make sure to name your collaborator in your submission (in the PDF of Problem 1).

If you have any questions, please ask!

The code for this assignment can be found in pset3-taisp.tar.gz. For this assignment you will be working in Python, using the CVC5 library, which implements the Sygus solver. For an example of how to use the CVC5 library, see the file q2/example.py. Full documentation can be found here. Note that since we are using the Sygus solver, you must use the Base Python API, not the Pythonic API.

The goal of the second problem will be to synthesize invariants necessary to prove that a piece of code is correct. We will be working in the context of a very simple language involving variables, simple arithmetic operations, and a set of simple commands (if, while, assignment and sequential composition). You will implement this in two parts, first, you will generate the verification condition as an AST using the same AST nodes provided to you for representing the program, and then you will generate CVC5 code and solve from this AST.

a) VC as an AST: For this part, you may need to introduce additional Expr nodes in order to represent the unknown invariants and to indicate the variables that may be used by this. Other than that, this should be a relatively straightforward implementation of verification condition generation. To check your work, ensure that

python q2/q2.py 2a

runs without errors.

b) Verification using CVC5: For the second part, you will need to implement two functions. First, on each Expr node, implement to_cvc5 which takes an Expr and returns a CVC5 expression. The full list of Kinds is useful for determining what functions are available. Also look at q2/example.py for examples of how to use the CVC5 library. You will need to implement this for any Expr nodes you added in part a. Note that variables is a dictionary mapping variable names to CVC5 variables, and invariants is a dictionary mapping Expr nodes to CVC5 functions, like min/max from the example. Second, implement solve. In this function you will need to set up variables and invariants and then call to_cvc5 on the assumption and VC. To check your work, ensure that

python q2/q2.py 2b

runs without errors.

c) Test cases: You need to submit five test cases for which your system can generate interesting invariants. Place these in example_N for N from 2-6. You can run your code on these test cases by running

python q2/q2.py 2c

Note: the invariants you generate should be relatively shallow when thought of as trees, otherwise the solver won't find a solution quickly. For example, the following invariant does not work well:

x >= 0 && y >= 0 && 3x + 2y >= 0

Submission

Submit your code as a .tar.gz file containing:

• q2/
  • q2.py