兩層式程序設(shè)計(jì)環(huán)境中設(shè)計(jì)模式驗(yàn)證工具的設(shè)計(jì)與實(shí)現(xiàn).pdf

1、為了解決軟件體系結(jié)構(gòu)漂移和體系結(jié)構(gòu)侵蝕的問(wèn)題,英國(guó)艾塞克斯大學(xué)的Eden博士從理論上提出了一種新的程序設(shè)計(jì)范型——兩層式程序設(shè)計(jì)(TTP).通過(guò)對(duì)該理論的研究以及對(duì)傳統(tǒng)程序編譯器的思考,本文提出了一種新的方法用于構(gòu)建設(shè)計(jì)模式的形式化驗(yàn)證工具.該工具從概念上分為兩層,第一層為傳統(tǒng)編譯層;第二層為編譯擴(kuò)展層,該層使用傳統(tǒng)編譯層的信息對(duì)程序進(jìn)行設(shè)計(jì)模式的形式化驗(yàn)證.在編譯擴(kuò)展層中,同時(shí)考慮了程序的內(nèi)部抽象表示、連接映射的內(nèi)部表示以及設(shè)計(jì)模式規(guī)

2、格說(shuō)明的內(nèi)部表示,這樣就提高了工具的靈活性和可擴(kuò)展性.在對(duì)設(shè)計(jì)模式形式化驗(yàn)證之前,需要經(jīng)過(guò)設(shè)計(jì)模型生成、設(shè)計(jì)模式規(guī)格說(shuō)明解釋兩個(gè)步驟,本文主要對(duì)這兩個(gè)方面以及設(shè)計(jì)模式的形式化驗(yàn)證策略進(jìn)行了研究及探討.以此為基礎(chǔ),本文作者用面向?qū)ο蟮姆椒ㄔO(shè)計(jì)并實(shí)現(xiàn)了TTP環(huán)境中的設(shè)計(jì)模式驗(yàn)證工具DPV_TOOL(Design Pattern Verification Tool),其中的第二層規(guī)格說(shuō)明使用Eden博士提出的設(shè)計(jì)模式形式化描述語(yǔ)言LePUS.

3、論文工作主要有以下幾方面:1.通過(guò)對(duì)Java語(yǔ)言的具體分析,根據(jù)Eden提出的設(shè)計(jì)模型定義,研究了Java語(yǔ)言的設(shè)計(jì)模型表示法,它是設(shè)計(jì)模型生成的參照標(biāo)準(zhǔn).此外,還對(duì)LePUS規(guī)格說(shuō)明和連接映射的正規(guī)文法進(jìn)行了研究,這是設(shè)計(jì)模式規(guī)格說(shuō)明解釋的參照標(biāo)準(zhǔn).2.設(shè)計(jì)了工具的概念框架,并以此為基礎(chǔ)設(shè)計(jì)和實(shí)現(xiàn)了DPV_TOOL.此外,研究了新框架中的內(nèi)部數(shù)據(jù)結(jié)構(gòu)和驗(yàn)證算法設(shè)計(jì).3.應(yīng)用DPV_TOOL對(duì)兩個(gè)經(jīng)典的設(shè)計(jì)模式Factory Metho

4、d和Template Method進(jìn)行驗(yàn)證,并對(duì)驗(yàn)證結(jié)果進(jìn)行了分析.通過(guò)實(shí)例表明了所完成的研究、開(kāi)發(fā)和實(shí)現(xiàn)工作的可行性、正確性和有效性.LePUS是設(shè)計(jì)模式形式化工作中一個(gè)富有意義的嘗試,LePUS的優(yōu)點(diǎn)在于集合變量的表達(dá)和推理能力,但它尚處于發(fā)展完善中.TTP是軟件工程領(lǐng)域中一個(gè)全新概念,Eden博士領(lǐng)導(dǎo)的工作組也正在進(jìn)行TTP支持環(huán)境的研究開(kāi)發(fā),曾預(yù)期在2003年9月完成一個(gè)原型.本論文及其相關(guān)工作獨(dú)立地從一個(gè)方面表明了LePUS和