一元多項(xiàng)式不等式似然不變量檢測(cè)方法研究.pdf

1、計(jì)算機(jī)技術(shù)發(fā)展至今，計(jì)算機(jī)軟件系統(tǒng)雖然只經(jīng)歷了短短的幾十年歷史，但其在社會(huì)各個(gè)行業(yè)得到了極其廣泛的應(yīng)用，如醫(yī)療衛(wèi)生、航空航天、核電站控制等等。同時(shí)，人們對(duì)軟件的質(zhì)量和安全有了更為廣泛和熱切的關(guān)注。如何提高軟件質(zhì)量，成為人們研究的熱點(diǎn)，并取得了一定的成績?；诤霞s的程序設(shè)計(jì)是提高軟件質(zhì)量的一種重要技術(shù)，且得到了非常廣泛的發(fā)展和應(yīng)用。合約描述了程序內(nèi)部的基本屬性，運(yùn)行的先決條件以及期望的運(yùn)行結(jié)果。從不同的層面合約可分為語法合約、數(shù)據(jù)合約、行

2、為合約和服務(wù)合約。程序不變量一般包含類不變量、前置條件和后置條件，它是一種基本的合約。程序不變量對(duì)于程序演進(jìn)與重構(gòu)、程序測(cè)試與排錯(cuò)、輔助定理證明、構(gòu)件升級(jí)替換都有重要作用。通過分析關(guān)鍵點(diǎn)上的不變量，可以檢測(cè)到程序運(yùn)行中的異常。程序不變量的動(dòng)態(tài)生成技術(shù)是解決合約形式化制定的一種有效方法。程序不變量動(dòng)態(tài)生成技術(shù)，可以進(jìn)行程序不變量的動(dòng)態(tài)檢測(cè)，分析程序各變量之間的關(guān)聯(lián)屬性，是提高程序質(zhì)量和規(guī)范程序代碼的關(guān)鍵。
　　本文重點(diǎn)研究了如何使用

3、動(dòng)態(tài)檢測(cè)技術(shù)發(fā)現(xiàn)程序中的一元多項(xiàng)式不等式似然不變量。論文首先介紹了基于合約的程序設(shè)計(jì)，由此引出了程序似然不變量動(dòng)態(tài)檢測(cè)技術(shù)。接著重點(diǎn)介紹了程序似然不變量動(dòng)態(tài)檢測(cè)技術(shù)及其主要的實(shí)現(xiàn)工具Daikon,并分析了Daikon在不變量檢測(cè)方法上存在的不足之處。然后針對(duì)現(xiàn)存不變量檢測(cè)工具的缺陷，提出了一元多項(xiàng)式不等式似然不變量發(fā)現(xiàn)規(guī)則和檢測(cè)算法，用實(shí)驗(yàn)驗(yàn)證了檢測(cè)算法對(duì)于一元多項(xiàng)式不等式似然不變量檢測(cè)的有效性，并與Daikon不變量檢測(cè)工具進(jìn)行了比較