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_2

2. Logic

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

In this chapter, we will cover two of the most important branches of mathematical logic.

2.1 Propositional Logic

We’ve seen a very brief example of how Dafny incorporates some sort of logic within it. In this section, we’ll cover logic in more detail.

The most basic level of logic is propositional logic that deals with the study of statements, sentences that are either true (⊤) or false (⊥). More specifically, here’s the description of these statements (formulas):

1. 1.

   The logical constants ⊤ and ⊥ ...