Dept. of Computer and Information science, Linköping University
Last updated: Tue, 02 Dec 1997 11:03:00
Bonnier, S. and Heyer, T. (1997). COMPASS: A Comprehensible Assertion Method. Technical Report LiTH-IDA-R-97-01, Department of Computer and Information Science, Linköping University, Sweden. (bibtex),
Abstract: We present an approach for automatically generating relevant, focused questions to be asked during code inspection sessions. The method is based on Hoare-logic. The novel key idea is the introduction of informal predicates, which, though not having a formal definition, may have a perfectly legal and unique informal interpretation. Such predicates make it easier to express requirements in terms of assertions, while still allowing for the automatic derivation of verification conditions. Moreover, informal predicates enable reasoning about assertions and verifying verification conditions at a level which is suitable for man rather than machine.