
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.