發(fā)布時(shí)間：2017-11-02 13:07

  本文關(guān)鍵詞：形狀圖理論的定理證明

  更多相關(guān)文章： 形狀圖邏輯 形狀分析 程序驗(yàn)證 自動(dòng)定理證明 循環(huán)不變式的推斷

【摘要】：驗(yàn)證操作易變數(shù)據(jù)結(jié)構(gòu)的指針程序仍面臨很多挑戰(zhàn).數(shù)據(jù)結(jié)構(gòu)中嚴(yán)重的指針別名顯著地復(fù)雜化對(duì)操作這些結(jié)構(gòu)的程序的推理.為分析和驗(yàn)證操作易變數(shù)據(jù)結(jié)構(gòu)的指針程序,文中提出了形狀圖邏輯.形狀圖是描述程序中靜態(tài)聲明的堆指針變量和動(dòng)態(tài)分配的結(jié)構(gòu)體中指針域變量的指向的一種有向圖,能準(zhǔn)確表達(dá)指針的有效性和指針之間的相等性,可用于判斷兩個(gè)訪問(wèn)表達(dá)式是否是別名.形狀圖邏輯是Hoare邏輯的一種擴(kuò)展,是一種直接將形狀圖作為程序中指針斷言集的程序邏輯.該文研究形狀圖的等價(jià)理論和蘊(yùn)含理論以及它們的判定方法和應(yīng)用.首先,把形狀圖及其等價(jià)規(guī)則和蘊(yùn)含規(guī)則分別類(lèi)比為代數(shù)項(xiàng)及其等式規(guī)則和重寫(xiě)規(guī)則,像研究代數(shù)規(guī)范的理論那樣來(lái)研究形狀圖理論.該文定義了形狀圖的語(yǔ)法理論和語(yǔ)義理論,定義了形狀圖重寫(xiě)系統(tǒng)及其終止性、局部合流性和合流性,然后得到基于形狀圖重寫(xiě)的形狀圖等價(jià)判定和蘊(yùn)含判定的方法.其次,提出循環(huán)不變形狀圖和遞歸函數(shù)前后形狀圖的自動(dòng)推斷方法.借助形狀圖理論的判定方法,該文把一個(gè)基于抽象解釋的推斷循環(huán)不變式的一般方法改編成推斷循環(huán)不變形狀圖的方法.由于計(jì)算終止的遞歸函數(shù)總有非遞歸的出口,可以先通過(guò)非遞歸路徑得到函數(shù)的后形狀圖的初值,然后再在遞歸路徑上迭代求解.從而,可以像推斷循環(huán)不變形狀圖那樣來(lái)推斷遞歸函數(shù)的前后形狀圖.第三,參照Nelson-Oppen框架,提出形狀圖理論和整數(shù)理論組合的一種判定方法.對(duì)易變數(shù)據(jù)結(jié)構(gòu),除了關(guān)心數(shù)據(jù)結(jié)構(gòu)各節(jié)點(diǎn)是否連成預(yù)定的形狀外,往往還關(guān)心數(shù)據(jù)在這些節(jié)點(diǎn)間的排列等特性,它們不能脫離易變數(shù)據(jù)結(jié)構(gòu)的形狀特征而單獨(dú)驗(yàn)證.為此,所提出的組合判定方法針對(duì)這類(lèi)程序的驗(yàn)證條件的特點(diǎn),利用程序分析階段得到的形狀圖對(duì)驗(yàn)證條件的前件中的符號(hào)斷言按形狀圖的節(jié)點(diǎn)分組;然后運(yùn)用整數(shù)理論為各節(jié)點(diǎn)推導(dǎo)出盡可能多的性質(zhì);最后才交由定理證明器Z3去自動(dòng)驗(yàn)證.這種方式有效地避免驗(yàn)證條件證明過(guò)程的不終止.基于形狀圖邏輯以及文中的工作,我們所開(kāi)發(fā)的程序驗(yàn)證系統(tǒng)原型減輕了自動(dòng)定理證明器的負(fù)擔(dān),并且能驗(yàn)證易變數(shù)據(jù)結(jié)構(gòu)上較為復(fù)雜的程序,如有序循環(huán)雙向鏈表、二叉排序樹(shù)、伸展樹(shù)、樹(shù)堆、二叉平衡樹(shù)和AA樹(shù)的插入和刪除函數(shù).
【作者單位】： 中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;中國(guó)科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室;
【關(guān)鍵詞】： 形狀圖邏輯 形狀分析 程序驗(yàn)證 自動(dòng)定理證明 循環(huán)不變式的推斷
【基金】：國(guó)家“八六三”高技術(shù)研究發(fā)展計(jì)劃項(xiàng)目基金(2012AA010901) 國(guó)家自然科學(xué)基金(61170018,61229201)資助~~
【分類(lèi)號(hào)】：TP311.1
【正文快照】： 科學(xué)基金(61170018,61229201)資助.張昱,女,1972生,博士,副教授,中國(guó)計(jì)算機(jī)學(xué)會(huì)(CCF)高級(jí)會(huì)員,主要研究方向?yàn)槌绦蛟O(shè)計(jì)語(yǔ)言的理論和實(shí)現(xiàn)技術(shù)、程序驗(yàn)證、確定性并行編程模型與運(yùn)行時(shí)系統(tǒng).E-mail:yuzhang@ustc.edu.cn.陳意云,男,1946年生,教授,博士生導(dǎo)師,中國(guó)計(jì)算機(jī)學(xué)會(huì)(CCF)

【相似文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前10條

1 王洪君,任秀麗;基于對(duì)象形狀特征的圖象檢索[J];松遼學(xué)刊(自然科學(xué)版);2001年03期

2 高飛;形狀特征的表示[J];計(jì)算機(jī)輔助工程;1995年02期

3 王春河,張鐵昌;面向集成化的形狀特征分類(lèi)與表示[J];航空學(xué)報(bào);1996年02期

4 王春河,周濟(jì),張新訪,張鐵昌;凸起形狀特征在集成過(guò)程中的處理技術(shù)[J];計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào);1996年04期

5 張煒,杜曉榮,張蕊;形狀特征的顯示表達(dá)框架的構(gòu)造[J];微機(jī)發(fā)展;1998年06期

6 賀雙拾;辛玉林;倪友平;陳曾平;;基于灰度圖形狀特征的低分辨雷達(dá)架次判別[J];雷達(dá)科學(xué)與技術(shù);2008年01期

7 廖凱寧;李志強(qiáng);孫靜;;基于形狀特征描述算子的3D模型檢索[J];計(jì)算機(jī)工程;2010年12期

8 高飛，，葉尚輝;形狀特征的定義[J];計(jì)算機(jī)輔助工程;1994年01期

9 曹尚穩(wěn);兩類(lèi)形狀特征的語(yǔ)義差及其操作互換性[J];系統(tǒng)工程與電子技術(shù);1999年07期

10 趙書(shū)蓮;宿曉華;;基于概念的形狀分類(lèi)與識(shí)別[J];電腦知識(shí)與技術(shù);2009年06期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù) 前6條

1 張世學(xué);吳恩華;;基于形狀特征與變形保持的動(dòng)態(tài)模型簡(jiǎn)化[A];中國(guó)計(jì)算機(jī)圖形學(xué)進(jìn)展2008--第七屆中國(guó)計(jì)算機(jī)圖形學(xué)大會(huì)論文集[C];2008年

2 高劑斌;李裕梅;;基于復(fù)雜網(wǎng)絡(luò)的圖像形狀特征提取及多特征融合方案探究[A];中國(guó)系統(tǒng)工程學(xué)會(huì)第十八屆學(xué)術(shù)年會(huì)論文集——A12系統(tǒng)科學(xué)與系統(tǒng)工程理論在各個(gè)領(lǐng)域中的應(yīng)用研究[C];2014年

3 胡帆;廖斌;薛巧平;;基于輪廓的形狀特征提取方法[A];2011年通信與信息技術(shù)新進(jìn)展——第八屆中國(guó)通信學(xué)會(huì)學(xué)術(shù)年會(huì)論文集[C];2011年

4 路陽(yáng);董宏麗;;基于MATLAB實(shí)現(xiàn)水稻顆粒圖像形狀特征分析[A];黑龍江省計(jì)算機(jī)學(xué)會(huì)2007年學(xué)術(shù)交流年會(huì)論文集[C];2007年

5 李連;朱愛(ài)紅;;基于形狀的圖像檢索技術(shù)研究[A];’2004計(jì)算機(jī)應(yīng)用技術(shù)交流會(huì)議論文集[C];2004年

6 甘俊英;趙向陽(yáng);張有為;;視覺(jué)語(yǔ)言特征—灰度輪廓權(quán)向量差分形狀特征[A];圖像 仿真 信息技術(shù)——第二屆聯(lián)合學(xué)術(shù)會(huì)議論文集[C];2002年

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前2條

1 程春;畫(huà)面清新自然 寓意美好吉祥[N];中國(guó)集郵報(bào);2014年

2 黨耀武;給你一雙“慧眼”　判讀高空偵察照片[N];中國(guó)國(guó)防報(bào);2002年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 趙偉;自由形狀特征的重用與抑制[D];浙江大學(xué);2008年

2 王青;反求工程中基于變形的自由形狀特征重構(gòu)[D];浙江大學(xué);2006年

3 陳飛;基于形狀先驗(yàn)的同時(shí)分割與識(shí)別研究[D];浙江大學(xué);2013年

4 柴倫紹;具有形變魯棒性的形狀特征研究及其在檢索中的應(yīng)用[D];北京郵電大學(xué);2014年

5 桂江生;二維水果形狀檢測(cè)與分類(lèi)算法研究[D];浙江大學(xué);2007年

6 賈棋;形狀不變特征提取及應(yīng)用研究[D];大連理工大學(xué);2014年

7 羅磊;形狀分解和基于機(jī)器學(xué)習(xí)的圖像檢索技術(shù)研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2013年

8 王軍偉;融合全局與局部信息的形狀輪廓特征分析與匹配[D];華中科技大學(xué);2012年

9 陳國(guó)棟;面向機(jī)器人的物體形狀及姿態(tài)識(shí)別研究[D];哈爾濱工業(yè)大學(xué);2011年

10 王淳;形狀的部分結(jié)構(gòu)解析和識(shí)別[D];華中科技大學(xué);2014年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 王松鶴;2D形狀中分支結(jié)構(gòu)的檢測(cè)[D];大連海事大學(xué);2015年

2 周斌;基于圖像形狀特征量的計(jì)算機(jī)輔助肝硬化檢測(cè)研究[D];廣西大學(xué);2015年

3 張倩;基于支持向量機(jī)的多特征交通標(biāo)志識(shí)別的研究與實(shí)現(xiàn)[D];東北大學(xué);2014年

4 李龍卓;基于形狀特征的圖像檢索技術(shù)研究[D];青島科技大學(xué);2015年

5 江靜宇;非剛體三維殘缺模型的形狀分類(lèi)算法研究[D];北京交通大學(xué);2016年

6 王璐;三維耳廓點(diǎn)云形狀特征提取及匹配[D];遼寧師范大學(xué);2015年

7 劉春爽;基于植物葉形狀和葉脈的植物葉自動(dòng)分類(lèi)研究[D];浙江理工大學(xué);2016年

8 顧華;基于形狀特征的人臉?lè)诸?lèi)研究[D];清華大學(xué);2004年

9 李國(guó)琳;傅立葉描繪子對(duì)形狀進(jìn)行識(shí)別與檢索[D];吉林大學(xué);2005年

10 陳孝春;二維形狀的描述和識(shí)別的研究[D];浙江大學(xué);2006年

本文編號(hào)：1131663