SDL中ADT的CHILL实现与证明

The Implementation and Its Correctness of Abstract Data Types in SDL with CHILL

软件生产自动化是人们长期追求的目标。如今,在通信领域,软件自动化生产已成为现实。本文着重描述SDL到CHILL变换中,抽象数据类型(ADT)的CHILL实现,并证明了这种实现的正确性(使用IF-THEN-ELSE重写规则)。同时,我们提出了用CHILL实现ADT的一般方法。

Software automatic generation is the goal for software engineers. Now, it is possible to automatically generate software in the field of communication. This paper focuses on the description of transformation of Abstract Data Types (ADT) from SDL to CHILL, and the methodology of the transformation. Then, we proof our transformation's correctness through some IF-THEN-ELSE rules. We also put forward ths general method for the realization of ADT with CHILL, through the CHILL internal structure.