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_8

8. Verification Exercises

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

In this chapter, we will provide exercises that can be used to both test your skills and further show what can be proven with Dafny, on the more practical side. For each of the exercises, we will provide its corresponding solution.

8.1 An Odd Implementation

  Exercise 1 Write a predicate OddPred that takes a nat and returns true if the number is odd, and false otherwise. Test your ...