Specifications, as a special form of computation, allow us to be precise by verifying that some existing computation performs the desired result. In this chapter, we will cover the details behind specifications.
Definition 1 Hoare logic
is a formal system that allows to reason about the correctness of computer programs. The key feature of Hoare logic is the Hoare triple ...Get Introducing Software Verification with Dafny Language: Proving Program Correctness now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
Get Mark Richards’s Software Architecture Patterns ebook to better understand how to design components—and how they should interact.
Dive in for free with a 10-day trial of the O’Reilly learning platform—then explore all the other resources our members count on to build skills and solve problems every day.
Start your free trial Become a member now