embodies a particular programming methodology and carries it to the level of complete formalization and implementation. However, one can use the system and employ the methods at various levels of rigor. It is possible to program in in a freewheeling manner with no attention to correctness; it is also possible to state only some properties that a program will satisfy and to present only the barest sketch of an argument that the program meets these specifications. On the other hand, in the same system one can also tighten control over the program step by step and level by level until there is a completely finished machine--checked proof that the program meets its specifications. In a sense the entire book illustrates this methodology, but in chapter 11 there are examples which relate our methods to those of the more popularly exposited school of E. W. Dijkstra, C. A. R. Hoare, E. C. R. Hehner, D. Gries and others [Dijkstra 76,Hoare 72,Gries 81,Hehner 79].