軟件體系結(jié)構(gòu)精化和代碼生成的自動(dòng)化.pdf

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

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

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