[發(fā)明專利]源代碼等價性驗(yàn)證裝置以及源代碼等價性驗(yàn)證方法

有效

• 申請?zhí)枺?/td>: 201380078502.X
• 申請日: 2013-08-28
• 公開（公告）號: CN105408872B
• 公開（公告）日: 2017-11-24
• 發(fā)明（設(shè)計）人: 鈴木康文;新原敦介;市井誠;野口秀人
• 申請（專利權(quán)）人: 株式會社日立制作所
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京銀龍知識產(chǎn)權(quán)代理有限公司11243
• 代理人: 范勝杰,王立杰

技術(shù)領(lǐng)域

本發(fā)明涉及一種源代碼等價性驗(yàn)證裝置以及源代碼等價性驗(yàn)證方法，尤其涉及一種在軟件重構(gòu)中為了防止因重構(gòu)實(shí)施導(dǎo)致的不良混入，在通過符號執(zhí)行方法驗(yàn)證作為程序的動作等價的情況下，用于防止計算量的爆發(fā)式增加，迅速驗(yàn)證重構(gòu)的正當(dāng)性的優(yōu)選的源代碼等價性驗(yàn)證裝置以及源代碼等價性驗(yàn)證方法。

背景技術(shù)

近年來，隨著信息處理社會發(fā)展，軟件系統(tǒng)浸透到一般社會，對于軟件要求的可靠性成為非常高的問題。另一方面，軟件隨著常年的差異/派生開發(fā)而踏上復(fù)雜化且大規(guī)模化的方向，軟件的易擴(kuò)展性或易理解性等維護(hù)性下降成為問題。

重構(gòu)是在非專利文獻(xiàn)1至3中所公開的方法，通過不改變軟件的動作地變更內(nèi)部結(jié)構(gòu)來改善軟件的設(shè)計品質(zhì)的方法的總稱，是減輕復(fù)雜度提高維護(hù)性的方法。該重構(gòu)的方法是對于確保踏上復(fù)雜化以及大規(guī)模化的方向的軟件的維護(hù)性有希望的技術(shù)，但由于變更源代碼，因此存在新混入不良的可能性。具體而言，在重構(gòu)中存在被分類為多個模式的方法，明示或暗示地決定各源代碼的變更順序以及針對用于保證通過該變更不會改變軟件的動作的源代碼的條件。在不按照該變更順序地變更了源代碼的情況下，或者，變更了不遵從這樣的條件的源代碼的情況下，不保證不改變成為對象的軟件動作，因此有可能在軟件中混入不良。因此，軟件開發(fā)者在軟件的維護(hù)階段，有擔(dān)心因重構(gòu)原因而在準(zhǔn)確地動作的軟件中混入不良，而做出不進(jìn)行重構(gòu)的判斷的可能性。因此，在軟件的維護(hù)階段，為了積極地進(jìn)行重構(gòu)，要求驗(yàn)證沒有由重構(gòu)導(dǎo)致的不良的混入的方法。

在非專利文獻(xiàn)3中，定義了72種典型使用的重構(gòu)模式(以下，簡單稱為“重構(gòu)模式”)。

在本說明書中，將兩個源代碼外在的動作相同，即針對相同輸入在執(zhí)行時得到相同輸出定義為兩個源代碼“等價”，將驗(yàn)證重構(gòu)實(shí)施前的源代碼和重構(gòu)實(shí)施后的源代碼等價稱為“等價性驗(yàn)證”。

作為驗(yàn)證重構(gòu)實(shí)施前的源代碼和重構(gòu)實(shí)施后的源代碼等價的方法所要求的條件，有如下的條件。

(1)一個條件是其作業(yè)的大部分被自動化，基于人工的作業(yè)較少。以往，通過基于人工的評價或測試來驗(yàn)證源代碼的等價性。通過對其實(shí)現(xiàn)基于工具的自動性驗(yàn)證，削減驗(yàn)證用時，促進(jìn)重構(gòu)。

(2)另一個條件是通過重構(gòu)驗(yàn)證方法判斷為動作等價或非等價的情況下，向開發(fā)者提示成為其根據(jù)的信息。通過向開發(fā)者提示易懂的成為判定基準(zhǔn)的信息，開發(fā)者自身能夠進(jìn)行再驗(yàn)證，針對工具的可靠性提高，促進(jìn)重構(gòu)。

作為等價性驗(yàn)證的方法，有：通過專利文獻(xiàn)1公開的源代碼比較，對產(chǎn)生差異的部分實(shí)施測試，比較其結(jié)果的方法；通過圖表表現(xiàn)非專利文獻(xiàn)1公開的源代碼，每次重構(gòu)時驗(yàn)證圖表否滿足所決定的事先條件的方法；以及使用非專利文獻(xiàn)2公開的符號執(zhí)行，來驗(yàn)證動作被保持的方法。

現(xiàn)有技術(shù)文獻(xiàn)

專利文獻(xiàn)

專利文獻(xiàn)1：美國專利申請公開第2007/0033576號說明書

非專利文獻(xiàn)

非專利文獻(xiàn)1：T.Mens,S.Demeyer,D.Janssens,"Formalising Behaviour Preserving Program Transformations",Proceedings of the First International Conference on Graph Transformation,USA,2002

非專利文獻(xiàn)2：S.Person,M.B.Dwyer,S.Elbaum,C.S.Pasareanu,"Differential Symbolic Execution",Proc.of ACM SIGSOFT Symposium on the Foundations of Software Engineering 2008,USA,2008

非專利文獻(xiàn)3：M.Fowler et al.,“Refactoring:Improving the Design of Existing Code”,USA,Addison-Wesley Professional,1edition,July 8,1999

發(fā)明內(nèi)容

發(fā)明要解決的課題

在非專利文獻(xiàn)1中公開了如下的方法：用圖表表現(xiàn)程序的方法調(diào)用關(guān)系，每次重構(gòu)時驗(yàn)證是否滿足所決定的事先條件。在該方法中，通過結(jié)構(gòu)上的驗(yàn)證實(shí)現(xiàn)動作的驗(yàn)證，因此每次重構(gòu)時，嚴(yán)密地定義其操作后收羅不會對動作產(chǎn)生影響的條件。因此，事實(shí)上，存在必須通過工具使重構(gòu)自動化，不能用于通過可能錯誤進(jìn)行重構(gòu)操作其本身的人工的重構(gòu)驗(yàn)證的問題。