Verifying Selection Sort: An Introduction to Program Verification in Dafny
dafny.org