next up previous contents index
Next: Environments Up: Research Topics Previous: Semantics

Methodology and Verification

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].

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995