COMMENTS ON A PAPER BY NEUHOLD AND STUDER

The authors of [5] described their experience in applying Hoare's method of program verification to an existing program. They reported two difficulties. The first was that certain Boolean expressions occurring in conditional or while statements needed to be strengthened to enable verification. This claim is false, and their three putative examples are refuted. The second difficulty was that the program had to be modified to use very restricted forms of jumps and procedures. Re this, we document recent work which enables these restrictions to be lifted. © 1979 Springer-Verlag.