Safety Properties

The most fundamental attribute of any program is “correctness”. Correctness has many interpretations, ranging from the narrow technical ones —the kind advocated in this book— to esoteric science-fiction notions that require a machine to mimic human behavior. In this book, we develop the theory for two major classes of program properties: safety and progress. We study safety properties in this chapter, and progress in the next chapter, for the programming model of chapter 2. A new class of properties, called maximality, is introduced in chapter 7. Logics for program composition are developed in chapters 8 and 9. In chapter 12, we extend the logic for the full programming model of chapter 3. In each chapter, we develop the theory —which is typically quite small— and apply the theory to a variety of examples to show its effectiveness.