This example sets up the formulation of a sequential bubble-sorting algorithm in PVS and
its proof of correctness. For more information see the
Array Sorting Tutorial[PDF][PVS]
Consult with the instructor before undertaking this project.
For addtional credit, verify another sorting algorithm, preferably one that is better than
Ο(n2)