CSCI P415/515 Wed Feb 29 13:39:23 EST 2012 [SDJ]

Homework Assignment


  1. Copy PVS source file sort.pvs into your working directory.
  2. The sorting_tutorial_1 theory defines two list-sorting functions called BubbleSort and InsertionSort
  3. In order to prove these results, you will need to prove some lemmas. The lemmas provided in the file are sufficient to prove BubbleSort_sorts. Additional lemmas will be needed to prove InsertionSort_sorts.
  4. Submit your .pvs, .prf and .status files to the SVN as usual.

Notes and Hints: