基于构件设计的正确性验证

CORRECTNESS VERIFICATION OF COMPONENT BASED PROGRAMS

本文研究基于构件设计的正确性问题．我们首先建立一个构件描述的模型：（１）接口：通过对ＣＯＲＢＡ的ＩＤＬ进行扩展，使其能够在构件的接口中同时描述构件的语法和语义信息；（２）实现：通过引入一个简单的程序模型，阐述如何利用子构件构造一个新的构件．然后我们考虑如何将构件的接口和实现联系起来：利用Ｈｏａｒｅ逻辑，验证一个构件的实现是否满足其接口中所给出的语义要求．

In this paper, we study the problems of correctness for the component based design. We firstly build a model of describe a component: (1)interface: Extending the IDL of CORBA so that it can describe both syntax and semantics of components; (2)implementation: Introducing a simple program model to tell how to construct a new component in terms of sub components. Then we consider how to relate the interface of a component to its implementation: Verify if the implementation of a component is satisfied with the requst of semantics in its interface by using Hoare logic.