SIGCSE Workshop 2012

Instructional Video Series

This three video series demonstrates how to formally prove the correctness of a simple operation.


Building a Reasoning Table – demonstrates how to build a reasoning table for a simple operation.


Generating VCs – uses the reasoning table from Video #1 to demonstrate how to generate the verification conditions for the operation.


Proving VCs – demonstrates how to prove the correctness of the operation by proving the verification conditions generated in Video #2.

Exercises

  • Integer_Do_Nothing_Unsolved.pdf
    This pdf contains a worksheet for doing the proof for the operation Do_Nothing discussed in the video series. Print it out and work the proof yourself to discover where you have weaknesses in your understanding.
  • Integer_Do_Nothing_Solved.pdf
    This pdf contains the solution to the worksheet. Use this to check your answers.