Abstract: Implicit invocation has become an important architectural style for large-scale system design and evolution. This paper addresses the lack of specification and verification formalisms for such systems. A formal computational model for implicit invocation is presented. We develop a verification framework for implicit invocation that is based on Jones' rely/guarantee reasoning for concurrent systems. The application of the framework is illustrated with several examples. The merits and limitations of the rely/guarantee paradigm in the context of implicit invocation systems are also discussed.

Abstract: Implicit invocation based on event announcement is an increasingly important technique for integrating systems. However, the use of this technique has largely been confined to tool integration systems---in which tools exist as independent processes---and special-purpose languages---in which specialized forms of event broadcast are designed into the language from the start. This paper broadens the class of systems that can benefit from this approach by showing how to augment general-purpose programming languages with facilities for implicit invocation. We illustrate the approach in the context of three different languages, Ada, C++, and Common Lisp. The intent is to highlight the key design considerations that arise in extending such languages with implicit invocation.