The use of ghost variables and virtual programming in the documentation and verification of programs
Maurice Clint, C. Vicent · Software Practice and Experience · 1984
Abstract Using 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.