Specification and Verification with References
Bruce W. Weide, Wayne D. Heym · 2001
Modern object-oriented programming languages demand that component designers, specifiers, and clients deal with references. This is true despite the fact that some programming language and formal methods researchers have been announcing for decades, in effect, that pointers/references are harmful to the reasoning process. Their wise counsel to bury pointers /references as deeply as possible, or to eliminate them entirely, hasnt been heeded. What can be done to reconcile the practical need to program in the languages provided to us by the commercial powers-that-be, with the need to reason soundly about the behavior of component-based software systems ? By directly comparing specifications for value and reference types, it is possible to assess the impact of visible pointers/references. The issues involved are the added difficulty for clients in understanding component specifications, and in reasoning about client program behavior. The conclusion is that making pointers/references visible to component clients needlessly complicates specification and verification.