Premium
The use of ghost variables and virtual programming in the documentation and verification of programs
Author(s) -
Clint M.,
Vicent C.
Publication year - 1984
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/spe.4380140803
Subject(s) - correctness , pascal (unit) , assertion , programming language , computer science , documentation , software engineering
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.