Chapter 1: Basic Principles

This chapter introduces basic principles for reasoning about simple imperative programs. The principles are illustrated first using program reviews and direct interactions with code as are supported in conventional development methods. Then, we illustrate how many of the reasoning principles are supported by automated deduction techniques in the Logika verification tool.