Introducing Software Verification with Dafny Language: Proving Program Correctness

© The Author(s), under exclusive license to APress Media, LLC, part of Springer Nature 2022

B. SitnikovskiIntroducing Software Verification with Dafny Languagehttps://doi.org/10.1007/978-1-4842-7978-6_5

5. Proofs

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

In this chapter, we’ll dive deeper into mathematical proofs to get us prepared for applying them to prove software correctness within Dafny.

We will start with the most basic concept: substitution. It lies at the core of mathematics and, as such, plays an important role in mathematical proofs. Substitution consists of a systematic replacement of the appearances of a symbol with a certain value, and it can be applied in a variety of contexts involving formal systems.

  Definition 1 In an expression ...