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_7

7. Mathematical Induction

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

Mathematical induction was mentioned earlier briefly when we discussed Peano’s axioms. In this chapter, we will provide the exact definition of it.

  Definition 1 Mathematical induction is a proof method that is used to prove that a predicate 𝑃 (𝑛) is true for all natural numbers 𝑛. It consists of proving two parts: a base case and an inductive step.

• For the base case, we need to ...