1 What is This Assignment’s Purpose?🔗

In this assignment you will get experience proving small programs correct by hand. We will contrast this against other forms of program proof later in the semester. It is therefore important that you keep a copy of your solution for future reference!

2 Theme Song🔗

Promise by Laufey

3 Problem Setup🔗

Recall that we have seen the insertion sorting algorithm: a helper function to insert an element into a sorted list, and a sorting function that repeatedly calls it to insert each element into the right place. We have loosely argued for why this program correctly implements sorting.

4 Assignment🔗

Your task is to prove that it actually implements sorting. You may assume that we are sorting numbers into ascending (non-descending) order; the proof will generalize to other settings quite straightforwardly. You should use structural induction to complete your proof.

Because induction is not a prerequisite for the course, you are not expected to do this all by yourself, nor will you be penalized for not getting this completely right. What you should not do is offload the work to an AI assistant. Instead, please use staff hours to get help learning what you need, using the assignment both as motivation and as a concrete illustration of the concepts. Give it your best shot!

5 Starter🔗

Not applicable.