The use of ghost variables and virtual programming in the documentation and verification of programs

摘要

AbstractUsing ghost variables and virtual programming, a method for documenting programs which exhibit some common characteristics is presented. The annotations required are expressed in a powerful high level assertion language. The usefulness of these annotations is illustrated by the generation of verification conditions for some small example programs written in a dialect of Pascal. Demonstrations of the correctness of these programs are also given.