1、一個大型軟件的體系結(jié)構(gòu)應(yīng)該是一個分層次的體系結(jié)構(gòu)，每一層都是該軟件的一個體系結(jié)構(gòu)。位于最上層的體系結(jié)構(gòu)是最抽象的，位于最下層的體系結(jié)構(gòu)是最具體的，直接用于生成代碼，中間每一層都是它上層體系結(jié)構(gòu)的精化。這樣，一個體系結(jié)構(gòu)層次，通常是從最上層自頂向下對每個構(gòu)件、連接子逐步精化得到的。 目前，在軟件體系結(jié)構(gòu)精化領(lǐng)域，普遍認可的是，使用精化模式完成對軟件體系結(jié)構(gòu)構(gòu)件和連接子的精化。本文立足于軟件體系結(jié)構(gòu)精化領(lǐng)域，提出了一種新的算法，分別

2、用于體系結(jié)構(gòu)構(gòu)件和連接子的精化，并使用C++語言實現(xiàn)了該算法。該算法基于一階邏輯和CSP(CommunicatingSequentialProcesses)理論，它們都是用來描述構(gòu)件和連接子的語義的，一階邏輯可以很好地描述順序程序的語義部分，但缺乏描述并發(fā)事件的能力；CSP是專門為描述并發(fā)事件的進程而設(shè)計的，故而，并發(fā)程序語義部分用CSP來描述。具體來說，首先，將構(gòu)件的規(guī)范和連接子的連接信息形式化描述為一階邏輯，即計算機可以識別的形式。

3、對于連接子部分，還需要用進程符號來描述交互事件的時序控制邏輯；然后，利用消解原理，對轉(zhuǎn)化為計算機內(nèi)部表示的體系結(jié)構(gòu)定理、待證結(jié)論進行消解，將軟件體系結(jié)構(gòu)的精化問題轉(zhuǎn)換為定理的自動證明問題；再根據(jù)消解過程中生成的最一般合一替換以及對有用子句的跟蹤構(gòu)造消解證明樹，換成合一樹，進而從合一樹中抽取用于精化體系結(jié)構(gòu)的重要信息，對于連接子內(nèi)部并發(fā)進程代碼部分，CSP可以自動生成，這樣便完成了對構(gòu)件和連接子的自動精化。這些信息包括精化后體系結(jié)構(gòu)的那些