Getting Started with Dafny: A Guide
Koenig Jason, K. Rustan, Mirka Leino · NATO science for peace and security series. D, Information and communication security · 2012
Common program specification and verification build on concepts like method pre- and postconditions and loop invariants. These lectures notes teach those concepts in the context of the language and verifier Dafny.