軟件體系結構精化和代碼生成的自動化.pdf

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

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

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