• Examples from the book:
  • LinearSearch.pi, which decides whether an array contains a given integer. Solution.
  • BubbleSort.pi, which sorts an array of integers. Solution.
  • BinarySearch.pi, which decides whether a sorted array contains a given integer faster than LinearSearch.pi can do it. Solution.
• Exercises from the book:
  • Abs.pi.
  • InsertionSort.pi, another sorting algorithm.
  • MergeSort.pi, a faster and more interesting sorting algorithm. More challenging to prove correct.
  • QuickSort.pi, a faster and more interesting sorting algorithm. Much more challenging to prove correct. Partial solution.
  • UnsortedUnion.pi, which computes the union of two arrays in the obvious way.
  • SortedUnion.pi, which computes the union of two sorted arrays in a fairly obvious way.

Development of πVC was supported by the National Science Foundation under Grant Nos. CSR-0615449 and CNS-0411363, by Navy/ONR contract N00014-03-1-0939, and by a Sang Samuel Wang Stanford Graduate Fellowship. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation or the Navy/ONR.