Princeton University
COS 510: Programming Languages

Homework 9

Prove a correctness property of Insertion Sort using the Dafny system. The program you'll be proving is shown in the other pane.

Add a //README comment at the top describing who you helped (or got help from), and what kind of help. Safe your solution into a file sort.dfy, and upload it at right.