Assigned: May 26, 2015.

Due: 11pm, June 9, 2015.

The goal of this assignment is to familiarize yourself with using an automated verifier to check verification conditions. Verification conditions are mechanistic formalization of weakest preconditions that we discussed in lecture.

In this assignment, you will be writing verification conditions for a few programs, and using an SMT solver (Z3) to check the validity of your solutions. The purpose of this exercise is to get you familiarized with the Z3 solver and its input language, SMT-LIB2, which is the standard format for specifying Satisfiability Modulo Theories (SMT) problems.

For the problem set, you need to download Z3
and build (by running the included `configure`

script followed by `make`

).
You can either use your own machine or the department cluster (recycle, bicycle, etc).
An alternative is to use the Z3 web interface.

We have successfully built the latest version of Z3 (4.4.0) out of the box on the department cluster and will only support that platform. If you use other platforms, feel free to post questions on the discussion board in case others can help.

The Z3 homepage contains a very clear documentation describing the SMT-LIB2 language and how to use Z3. While that page has way more than what you need for this assignment, it might be a good idea to look through a few examples there to get a sense of the input SMT-LIB2 language. Below is a small example to help you get started.

;; ";" starts a comment line ;; define a scalar (enumerated) type person. Variables of type person can only ;; be equal to joe, jane, tim or tina. (declare-datatypes () ((person joe jane tim tina)) ) ;; define two variables p1 and p2 of type person (declare-const p1 person) (declare-const p2 person) ;; We declare-const two variables for the money owned by person p1 and the person p2 (declare-const p1money Int) (declare-const p2money Int) ;; Person 1 has more money than person 2 (assert (> p1money p2money)) ;; money amounts are positive (assert (and (< 0 p1money) (< 0 p2money))) ;; Person 1 can not be the same as person 2 (assert (not (= p1 p2))) ;; Jane must have more money than everyone else. (assert (=> (= p1 jane) (> p1money p2money))) (assert (=> (= p2 jane) (> p2money p1money))) ;; find a solution (check-sat) ;; Tell Z3 that we actually want to see the result, ;; not just to tell us whether it's sat or unsat (get-model)When you run the file above in Z3, you will get an assignment to p1, p2, p1money and p2money that satisfies all the constraints. For example, Z3 will return the following given the input above:

sat (model (define-fun p2money () Int 1) (define-fun p1 () person tim) (define-fun p2 () person joe) (define-fun p1money () Int 2) )However, if we add the following constraint, the problem becomes unsatisfiable (no assignment satisfies it because we previously said that jane has more money than everyone else and that p2money < p2money):

;; an unfeasible constraint (assert (= p2 jane))and the solver returns the following:

unsat

You are going to use Z3 to answer the following puzzle (courtesy of mathisfun.com):

You have three crates, one has only apples, one has only oranges, and
one has both apples and oranges. However, someone has maliciously
relabeled the crates, and all you know is that *all* the labels have
been shuffled, i.e., none of the crates has the right label. The goal is
to infer the right label by picking a single fruit from one of the
crates.

(a) (5 pts)
Suppose you picked a fruit out of the crate labeled "Mixed", and it
happened to be an apple. Write a Z3 formula involving the variables
`realApple`

, `realOrange`

and `realMixed`

,
such that the variable realOrange will
tell you the real contents of the crate labeled "orange", the variable
realApple will tell you the real contents of the crate labeled "apple", and
similarly for realMixed. The values of these three variables should be
consistent with the fact that you picked an apple from the mixed crate.

(b) (5 pts) Use the solver to prove that there is only one possible assignment for the labels given the information that you picked an apple from the mixed crate.

(c) (5 pts) If you had picked an apple from the crate labeled "orange" instead, would that information had been enough to uniquely determine the solution? Provide a formula that can answer this question.

Consider the following 4 verification problems. For each of them, hand-code the verification conditions in Z3, and show that they are correct (i.e., the post-condition is true given the precondition and the verification conditions). We are only concerned with partial correctness in these problems so you do not need to provide ranking functions for the loops.

Since we are not looking for a satisfying assignment or model (as in problem 1) in
program verification,
the usual strategy is to assert the preconditions to be true, and then assert
that the *negated* verification condition is
*not satisfiable*, and hence the original verification condition is true (this is also known as refutation-based proving).
This is especially important for first-order logic with
quantifications, as that is
undecidable in general.
It might take some time before the solver will come back with a satisfiable model.

Recall from lecture what we need to show for a program containing loops. Given
pre-condition **PRE** before entering the loop,
post-condition **POST** assuming the loop terminates, and loop invariant **I**,
we need to show that:

- the loop invariant is initially true before entering the loop:
**PRE**→**I** - the loop invariant is preserved if the loop continues:
**I**∧ loop condition is true → wp(c,**I**), where wp(c,**I**) is the weakest precondition of the body of the loop with**I**as the post-condition - the loop invariant implies the post condition if the loop terminates:
**I**∧ loop condition is false →**POST**

One way to structure your proof script is the following:

; declare any variable that you might need (declare-const ...) ; preconditions (assert ...) ; verification condition given the post-condition (assert (not (....))) (check-sat)Note: In the following

(a) (5 pts)

(b) (5 pts)// precondition: {y = y0 ∧ k = k0 ∧ t = y0 - k0}// invariant: {t = y - k0 ∧ k = k0}while (t > 0) { y = y - 1; t = t - 1; }// postcondition: {y ≤ k0}

(c) Come up with the invariant given the postcondition (10 pts)// precondition: {y < len ∧ Err = 0}// invariant: {y < len ∧ Err = 0}while (q < y) { if (q > len) { Err = 1; } q = q + 1; }// postcondition: {Err = 0}

Hint: you might want to define sum as an uninterpreted function quantified over integers. Its behavior can be defined using additional assertions similar to the function

`f`

shown in the tutorial.
(d) Come up with the invariant given the postcondition (10 pts)// precondition: {s = 0 ∧ x0 ≥ 0 ∧ x = x0}// invariant: ??while (x ≠ 0) { s = s + x; x = x - 1; }// postcondition: {s = Σ_{i = 0 → x0}i}

Hint: first decide on the relationship between the two loop invariants.

// precondition: {m = 0 ∧ x = x0 ∧ t = t0 ∧ t0 > 0 ∧ x0 ≥ 0}// outer loop invariant: ??while (t > 0) {// inner loop invariant: ??while (x > 0) { m = m + 1; x = x - 1; } t = t - 1; }// postcondition: {m = x0}

- a description of the bug.
- a minimal test case that reproduces the bug.

Please submit a separate Z3 proof script for each problem. For problem 1, you can submit all parts in the same file if you prefer. We will grade your proofs based on whether they are correct (obviously), and whether you have set up the proof correctly.

In a separate readme file, describe how long it took you to complete this assignment, and any comments regarding difficulty, usefulness, etc.