This volume provides a detailed comparison and study of the various methods for reasoning about software. The material offers a comprehensive understanding of which program structures are easier to manipulate by formal techniques.