The methods in this textbook for reasoning about programs are based on using formal logic to characterize program execution. Here, we review some rudiments of logic and show how logic can be used to formalize safety and liveness. Our study of logic is done from the programmer’s viewpoint, not the logician’s. For us, logic is simply a tool. However, as with most tools, it must be understood to be used effectively.
Unable to display preview. Download preview PDF.