Principles of Concurrent and Distributed Programming, Second Edition

Appendix B. Review of Mathematical Logic

Mathematical logic is used to state correctness properties and to prove that a program or algorithm has these properties. Fortunately, the logic needed in this book is not very complex, and consists of the propositional calculus (which is reviewed in this appendix) and its extension to temporal logic (Chapter 4). Variables in concurrent algorithms typically take on a small number of values, so that the number of different states in a computation is finite and relatively small. If a complicated calculation is required, it is abstracted away. For example, a concurrent algorithm may calculate heat flow over a surface by dividing up the surface into many cells, computing the heat flow in each and then composing ...