Homework Assignment

Instructions:

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
   • P415 students: Verify BubbleSort. Specifically, prove the corollary BubbleSort_sorts.
   • P515 students: Verify both BubbleSort and InsertionSort. Specifically prove BubbleSort_sorts and either InsertionSort_sorts and or InsertionSort_and_BubbleSort.
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:

• This theory uses the list[T] data type from the Prelude. PVS supports a special notation for constructing lists of this type. You can write (: 1, 2, 3 :) instead of cons(1, cons(2, cons(3, null))) to express a concrete list value.

• A translation of the PVS BubbleSort to Scheme is included (.SS). You could use this to test the function. Alternatively, the Prover command (eval "expression") will attempt to evaluate the given expression. For example, in the proof of Proposition check2 the command (eval "BubbleSort((: 3, 4, 1, 4, 2 :)) will (should) generate the line

  BubbleSort((: 3, 4, 1, 5, 2 :)) = (: 1, 2, 3, 4, 5 :)

  in the *pvs* buffer.

• I recommend that you work backward from BubbleSort_sorts. That way you will see how the lemmas apply before attempting to prove them. That is also the way the lemmas were conceived, for the most part.

• The assignment uses the slist: TYPE = list[int] theory from the Prelude. Have a look at the list and list_props theories in the Prelude to see what facts they contain about lists.

• Theory sorting_tutorial_1 begins by defining the two properties that a sorting algorithm should satisfy.

  1. Ordered?(L) A list of integers is ordered if its elements are in non-decreasing order.

  2. Permutation?(L₁, L₂) A list L₁ is a permutation of a list L₂ if the two lists contain the same elements in the same numbers.
  For example let L₁ = (1, 3, 2, 3, 5, 4, 1, 5) and L₂ = (1, 2, 3, 4, 5). L₂ is ordered but it is not a sorted version of L₁ because it has too few occurences of 1, 3 and 5. A correct sorting function would return the list L₃ =(1, 1, 2, 3, 3, 4, 5, 5)

• HINT: Focus on the Ordered? property first. It is easier to prove.

• BubbleSort Traverses a list, calling the help function Bubble, which does the actual work. The ordinary induction on BubbleSort_sorts and expanding Sorted? leads to the induction case:

  [-1] Ordered?(BubbleSort(L)) |------- {1} Ordered?(Bubble(K, BubbleSort(L)))

  and similarly for Permutation?

  Hence, the correctness of BubbleSort quickly reduces questions about Bubble, and as always, these questions need to be generalizations of the goal. Appropriate generalizations are given in Lemmas bubble_lemma_1, and bubble_lemma_2, but before you look at them, try to discover them yourself.

• As the comments point out, there are two approaches to verifying InsertionSort. The second, showing equivalence to BubbleSort, is probably the easier way, but I haven't done it so I'm not sure.