Results from work involving formal methods in software engineering often can be interpreted in the context of practical software engineering problems, and thereby contribute to solutions. One example of this phenomenon involves an understanding of the need for restrictions imposed by ``toy'' languages that admit modular program verification systems. This analysis can be applied to ``real'' languages that are ostensibly intended to support component reuse (e.g., Ada and C++). The result is that unless we restrict procedure calls in ways that are not — indeed, cannot be — checked or enforced by compilers for these languages as presently defined, it is impossible to develop a modular system for reasoning about program behavior. However, by adopting an alternate explanation of parameter passing, call-by-swapping, we can remove the procedure-call impediment to a modular reasoning system without restricting calls in any way.
Keywords: Reuse, software component, local certification, proof of
correctness, verification, aliasing, parameter passing, call-by-reference,
call-by-swapping
Workshop Goals: Learning; networking; having an opportunity to get
feedback from others on our ideas, and to provide same for others' ideas
Working Groups: Design guidelines for reuse, Reuse and OO methods, Reuse
and formal methods, Reusable component certification, Reuse handbook,
Education