CS156: piVC Homework

Download the piVC client from http://theory.stanford.edu/~jasonaue/pivc. (It is also located on the class AFS space at /usr/class/cs156/pivc.jar). You can run piVC either by double-clicking on the JAR file (if your OS supports that), or issuing the command java -jar <path_to_jar_file>. If you haven't already done so, make sure to read the tutorial, which is also posted on that site. There are also some sample programs that you can peruse if desired.

Submission is done electronically. When you have finished each problem, submit by clicking the "Submit" button in piVC.

Problem 1 is worth 25 points and problem 2 is worth 75 points. As long as you verify each program correctly (i.e. all VCs are green), you will get full points.

If you have questions about the piVC assignment, contact Jason Auerbach. His contact details and office hours can be found on the CS156 homepage.

Problem 1: Abs.pi

Starter file: http://theory.stanford.edu/~jasonaue/pivc/samples/Abs.pi.

Replace the @true annotation on the for loop with whatever is necessary to prove the postcondition. Do not change the precondition or postcondition.

This problem is similar to the problem on the tutorial. Treat it as a warm-up for the next problem.

Problem 2: InsertionSort.pi

Starter file: http://theory.stanford.edu/~jasonaue/pivc/samples/InsertionSort.pi.

Replace the @true annotations on the for loops with whatever is necessary to prove the postcondition. Do not change the precondition or postcondition.

This problem is more challenging than the first. It is important that you have an intimate understanding of how InsertionSort works you attempt to verify it.

There are many possible ways to prove the postcondition. Here are some hints for one possible way. Keep in mind that, depending on the approach you follow, you may not need to use all of these hints.

  1. What are the bounds of i and j? Specify these bounds in the loop annotations.
  2. After k iterations of the outer loop, the first k entries are sorted. Add an annotation to state this fact. You may need to include this information in the annotations for both the inner and outer loops.
  3. What do you know about the bounds of t? (Hint: notice that t must be greater than or equal to a specific element of the array.) Be sure to express this in the inner loop.
  4. If the inner loop has executed at least once (i.e. j<i-1), then you know an additional property of the array. Determine what this property is. You may want to use an implication (j<i-1 -> ...) to express this property.