6

Proof Rules—Basics

Objectives

After reading this chapter, you should understand:

  • The importance of Proof Rules (Axiomatic Semantics) in Program Verification
  • Assertions and their role
  • Proof Rules and their Notation
  • How Proof Rules are specified for standard High Level Language constructs
  • How to ensure correct Termination of Programs
  • Program Transformation: Why and How
  • Proof Rules for Procedures and Functions

Einstein argued that there must be simplified explanations of nature, because God is not capricious or arbitrary. No such faith comforts the software engineer.

—Fred Brooks

If builders built buildings the way programmers wrote programs, the first woodpecker that came along would destroy civilization.

—Author unknown

Chapter ...

Get Design and analysis of Algorithms, 2nd Edition now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.