Homework 07 - Due April 16

Problem 1

Select the topic of your project.

You may use current implementation homeworks as the starting point.

Here is a list of possible project suggestions, but you are free to choose your own.

Submit a project proposal of length 200-1000 words. Summarize project goal, why it is interesting, how you plan to solve it, and the difficulties you expect to encounter.

The proposal is not final–you can reformulate the project based on discussion with us.

Problem 2

Extend verification condition generator for integer programs from Homework03 to handle procedures with supplied procedure specifications as described in Lecture14.

Connect the verification condition generator to a theorem prover using the SMT-LIB interface. In your solution you may use this code DecisionProc.scala, generously provided by Damien from his previous homework.

Your resulting program should be able to check whether a given collection of recursive procedures that manipulate integers satisfies given preconditions and postconditions. Provide at least 3 test cases that illustrate the capabilities of the system.

For simplicity, you may assume that procedures do not return results, only accept parameters and change global state. There is no need to write a parser, use syntax trees.

Optional: insert assertions that check that no result of arithmetic operation produces number whose absolute value is larger than 2^15-1. Explore usability of the resulting system in practice.

Problem 3

Prove the following statement, which is a special case of a lemma used in quantifier elimination for set algebra.

Let $B_1, B_2$ be two finite disjoint sets and $L_1,L_2,K_1,K_2$ non-negative integers. Then the following two conditions are equivalent:

there exists a finite set $A$ such that: $|B_1 \cap A|=L_1$ , $|B_1 \setminus A|=K_1$ , $|B_2 \cap A|=L_2$ , and $|B_2 \setminus A|=K_2$ ;
$|B_1|=L_1+K_1$ and $|B_2|=L_2+K_2$ .