论文部分内容阅读
一个大型软件的体系结构应该是一个分层次的体系结构,每一层都是该软件的一个体系结构。位于最上层的体系结构是最抽象的,位于最下层的体系结构是最具体的,直接用于生成代码,中间每一层都是它上层体系结构的精化。这样,一个体系结构层次,通常是从最上层自顶向下对每个构件、连接子逐步精化得到的。
目前,在软件体系结构精化领域,普遍认可的是,使用精化模式完成对软件体系结构构件和连接子的精化。本文立足于软件体系结构精化领域,提出了一种新的算法,分别用于体系结构构件和连接子的精化,并使用C++语言实现了该算法。该算法基于一阶逻辑和CSP(CommunicatingSequentialProcesses)理论,它们都是用来描述构件和连接子的语义的,一阶逻辑可以很好地描述顺序程序的语义部分,但缺乏描述并发事件的能力;CSP是专门为描述并发事件的进程而设计的,故而,并发程序语义部分用CSP来描述。具体来说,首先,将构件的规范和连接子的连接信息形式化描述为一阶逻辑,即计算机可以识别的形式。对于连接子部分,还需要用进程符号来描述交互事件的时序控制逻辑;然后,利用消解原理,对转化为计算机内部表示的体系结构定理、待证结论进行消解,将软件体系结构的精化问题转换为定理的自动证明问题;再根据消解过程中生成的最一般合一替换以及对有用子句的跟踪构造消解证明树,换成合一树,进而从合一树中抽取用于精化体系结构的重要信息,对于连接子内部并发进程代码部分,CSP可以自动生成,这样便完成了对构件和连接子的自动精化。这些信息包括精化后体系结构的那些构件和连接子的内部互联,与体系结构原有部分的互联,以及旧体系结构的构件和连接子与新体系结构的构件和连接子之间的对应关系。在基于构件的软件开发过程中,可以利用该算法自动生成胶合代码。