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_9

9. Implementing a Formal System

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

So far, we have been mostly using a set of formal systems to prove software correctness. In this final chapter, we show how to both create and use a formal system in order to be able to prove facts. For that, we will provide a minimal implementation¹ of propositional logic, as described in Chapter 2. For a more advanced implementation of a formal system, see [7].

The syntax of the formal system expressed in BNF (Backus-Naur form) is

1  prop ::= P | Q | R | unop prop | prop ...