Home  |  Download  |  Tutorial  |  Pi Programs  |  Book

πVC Tutorial

New version available

This tutorial assumes that you are have read or are currently reading our textbook, The Calculus of Computation: Decision Procedures with Applications to Verification, particularly Chapter 5. The language Pi accepted by πVC varies slightly from the language defined in the book.

Proving that BubbleSort returns a sorted array

 Let's prove the correctness of BubbleSort.pi.
  1. Start πVC: cd pivc; ./bin/piVC &. Notice that you can drag the separator between the two panes.

  2. Open BubbleSort.pi: File &rarr Open.
  3. Compile it to make sure it's syntactically and semantically correct: Compile &rarr Compile. Modify the text to be incorrect; errors are reported in the "Raw Output" tab of the right pane. Restore the original text. Unfortunately, πVC is rarely as clear about errors as in the following figure.

  4. Run the program. Click on the "Debugger" tab in the right pane. Type BubbleSort([1;3;2]), and click "Evaluate". Explore the computation using the "start" (<<), "previous" (<), "next" (>), and "end" (>>) buttons at the bottom of the pane.

  5. Now add annotations to prove the correctness of BubbleSort.pi. Compile again and select the "Verification Conditions" tab of the right pane. Select a verification condition (VC) from the drop-down menus (the first selects the function; the second selects the VC). Notice that several are invalid. Select an invalid one. Observe that the related text is highlighted. The top of the "Verification Conditions" window also contains the associated basic path.

  6. Add annotations to make the specification inductive.

  7. Work through the other examples covered in Chapters 5 and 6.

Home  |  Download  |  Tutorial  |  Pi Programs  |  Book

© 2007, Aaron Bradley and Zohar Manna
Direct questions, comments, and cool Pi programs to arbrad{Shift+2}cs.stanford.edu.

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.