Program Proofs
This comprehensive and highly readable textbook teaches how to formally reason about computer programs using an incremental approach and the verification-aware programming language Dafny.