一種順序匯編指令程序驗(yàn)證方法與系統(tǒng) 技術(shù)領(lǐng)域 [0001] 本發(fā)明涉及的是一種順序匯編指令程序驗(yàn)證方法與系統(tǒng)，屬于軟件工程、形式化方法技術(shù)領(lǐng)域。 背景技術(shù) [0002] 計(jì)算機(jī)軟件由于設(shè)計(jì)、編碼等原因，常常出現(xiàn)錯(cuò)誤。通過測(cè)試可以發(fā)現(xiàn)部分的軟件錯(cuò)誤，也可以通過采用先進(jìn)的軟件工程技術(shù)減少錯(cuò)誤的產(chǎn)生。但是，迄今為止，這些方法都不能徹底根除軟件錯(cuò)誤。利用形式化方法驗(yàn)證軟件設(shè)計(jì)與軟件編碼之間的一致性，是目前業(yè)界公認(rèn)有可能徹底根除軟件錯(cuò)誤的一種方法。但是形式化方法非常耗費(fèi)時(shí)間，因此有必要提出一種使形式化工作的工作量大大減少的方法來驗(yàn)證軟件設(shè)計(jì)與編碼之間的一致性。 發(fā)明內(nèi)容 [0003] 本發(fā)明所要解決的技術(shù)問題是克服形式化證明與驗(yàn)證過程需要耗費(fèi)大量人力的問題，提供一種順序匯編指令程序驗(yàn)證方法。 [0004] 本發(fā)明為了達(dá)到以上的技術(shù)目的，所采用的技術(shù)方案如下： [0005] 在一個(gè)方面，本發(fā)明提供了一種順序匯編指令程序驗(yàn)證方法，包括如下步驟： [0006] 建立指令語義規(guī)則：對(duì)指令系統(tǒng)中用匯編語句表示的每一條指令建立一個(gè)語義規(guī)則； [0007] 建立順序匯編指令程序狀態(tài)空間：依次獲取順序匯編指令程序中操作數(shù)的地址a1，a2，...，aM、長度l1，l2，...，lM和初始數(shù)值x1，x2，...，xM；獲取的所有操作數(shù)的集合作為程序的工作集，程序的工作集中每個(gè)操作數(shù)都獲得一個(gè)數(shù)值后作為程序的一個(gè)狀態(tài)向量，程序的工作集中所有操作數(shù)的初始數(shù)值是程序的初始狀態(tài)向量，所有狀態(tài)向量構(gòu)成程序的狀態(tài)向量空間； [0008] 順序匯編指令程序語義規(guī)約：對(duì)于程序的每一條指令依次進(jìn)行語義規(guī)約；對(duì)于第j條指令，根據(jù)指令的指令助記符、源操作數(shù)和目標(biāo)操作數(shù)將程序的工作集中所有操作數(shù)的值都規(guī)約成由程序的初始狀態(tài)向量表示的新的狀態(tài)向量，并將新的狀態(tài)向量記為ej，1，ej，2，……，ej，M，其中j表示指令序號(hào)，j取值從1到N，N為指令總數(shù)，M表示所有操作數(shù)的總數(shù)； [0009] 語義證明腳本生成：依次對(duì)順序匯編指令程序中的指令根據(jù)指令的語義規(guī)則、指令執(zhí)行前的程序的狀態(tài)向量，生成指令執(zhí)行后新的狀態(tài)向量為規(guī)約出來的狀態(tài)向量ej，1，ej，2，……，ej，M的證明腳本。 [0010] 在以上技術(shù)方案中進(jìn)一步地，建立指令語義規(guī)則方法如下： [0011] 指令I(lǐng)表達(dá)式如下： [0012] 指令助記符源操作數(shù)，目標(biāo)操作數(shù) [0013] 指令執(zhí)行前的狀態(tài)向量s0表示為：s0.aj＝x0，j，j＝1，2，…，M； [0014] 指令執(zhí)行后的狀態(tài)向量s1表示為：s1·aj＝x1，j，j＝1，2，…，M； [0015] 其中aj程序的工作集中第j個(gè)操作數(shù)的地址，x0，j表示指令執(zhí)行前地址為aj的操作數(shù)的值，x1，j表示指令執(zhí)行后地址為aj的操作數(shù)的值，M是操作數(shù)的總數(shù)； [0016] 則指令I(lǐng)的語義規(guī)則為： [0017] I∧s1→(s1·aj＝s0·aj＝x0，j，j＝1，2，…，M，j≠v)∧s1·av＝exp(x0，u，x0，v)，其中u和v分別是指令的源操作數(shù)與目標(biāo)操作數(shù)的下標(biāo)；exp(x0，u，x0，v)表示由指令I(lǐng)執(zhí)行前s0的狀態(tài)分量x0，u，x0，v構(gòu)成的表達(dá)式，表達(dá)式exp是根據(jù)指令I(lǐng)的指令助記符確定。 [0018] 在以上技術(shù)方案中進(jìn)一步地順序匯編指令程序語義規(guī)約的方法如下： [0019] 假定程序的第j-1條指令后所有操作數(shù)的值已經(jīng)規(guī)約為x1，x2，...，xM的表達(dá)式ej- 1，1，ej-1，2，……，ej-1，M，第j條指令I(lǐng)j的語義為： [0020] s1(e+i)＝expi(s0(b)，...，s0(b+u-1)，s0(e)，...，s0(e+u-1))，i＝0，...，u-1，???(1-1) [0021] s1(d)＝s0(d)，d≠dst，...，d≠dst+u-1，???(1-2) [0022] 其中b是源操作數(shù)地址，e是目標(biāo)操作數(shù)地址；根據(jù)操作數(shù)的地址和長度，為s0(b)，…，s0(b+u-1)，s0(e)，…，s0(e+u-1)在ej-1，1，ej-12，……，ej-1M找到對(duì)應(yīng)的表達(dá)式，用它們?nèi)〈鶬j語義規(guī)則中的對(duì)應(yīng)的式子，得到指令I(lǐng)j執(zhí)行后s1表示的所有的操作數(shù)的值，它們都是初始值x1，x2，...，xM的表達(dá)式ej，1，ej，2，…，ej，M。 [0023] 在以上技術(shù)方案中進(jìn)一步地，語義證明腳本生成方法是： [0024] 為程序執(zhí)行前初始狀態(tài)向量s0＝(x1，x2，...，xM)建立一個(gè)表示其特征的謂詞公式：Q0(s0)＝“a1＝x1，...，aM＝xM，”； [0025] 在第j條指令執(zhí)行前，程序的狀態(tài)向量與操作數(shù)的初始值的之間的關(guān)系用一個(gè)邏輯公式Qj-1(s0，sj-1)表示，表達(dá)式如下：

1.一種順序匯編指令程序驗(yàn)證方法，其特征是包括如下步驟： 建立指令語義規(guī)則：對(duì)指令系統(tǒng)中用匯編語句表示的每一條指令建立一個(gè)語義規(guī)則； 建立順序匯編指令程序狀態(tài)空間：依次獲取順序匯編指令程序中操作數(shù)的地址a1，a2,…,aM、長度l1，l2,…,lM和初始數(shù)值x1，x2,…,xM；獲取的所有操作數(shù)的集合作為程序的工作集，程序的工作集中每個(gè)操作數(shù)都獲得一個(gè)數(shù)值后作為程序的一個(gè)狀態(tài)向量，程序的工作集中所有操作數(shù)的初始數(shù)值是程序的初始狀態(tài)向量，所有狀態(tài)向量構(gòu)成程序的狀態(tài)向量空間； 順序匯編指令程序語義規(guī)約：對(duì)于程序的每一條指令依次進(jìn)行語義規(guī)約；對(duì)于第j條指令，根據(jù)指令的指令助記符、源操作數(shù)和目標(biāo)操作數(shù)將程序的工作集中所有操作數(shù)的值都規(guī)約成由程序的初始狀態(tài)向量表示的新的狀態(tài)向量，并將新的狀態(tài)向量記為ej,1,ej,2,……,ej,M，其中j表示指令序號(hào)，j取值從1到N，N為指令總數(shù)，M表示所有操作數(shù)的總數(shù)； 語義證明腳本生成：依次對(duì)順序匯編指令程序中的指令根據(jù)指令的語義規(guī)則、指令執(zhí)行前的程序的狀態(tài)向量,生成指令執(zhí)行后新的狀態(tài)向量為規(guī)約出來的狀態(tài)向量ej,1,ej,2,……,ej,M的證明腳本。 2.根據(jù)權(quán)利要求1所述的一種順序匯編指令程序驗(yàn)證方法，其特征是，建立指令語義規(guī)則方法如下： 指令I(lǐng)表達(dá)式如下： 指令助記符源操作數(shù)，目標(biāo)操作數(shù) 指令執(zhí)行前的狀態(tài)向量s0表示為：s0.aj＝x0,j,j＝1,2,…,M； 指令執(zhí)行后的狀態(tài)向量s1表示為：s1.aj＝x1,j,j＝1,2,…,M； 其中aj程序的工作集中第j個(gè)操作數(shù)的地址，x0,j表示指令執(zhí)行前地址為aj的操作數(shù)的值，x1,j表示指令執(zhí)行后地址為aj的操作數(shù)的值，M是操作數(shù)的總數(shù)； 則指令I(lǐng)的語義規(guī)則為： I∧s1→(s1.aj＝s0.aj＝x0,j,j＝1,2,…,M,j≠v)∧s1.av＝exp(x0,u,x0,v)，其中u和v分別是指令的源操作數(shù)與目標(biāo)操作數(shù)的下標(biāo)；exp(x0,u,x0,v)表示由指令I(lǐng)執(zhí)行前s0的狀態(tài)分量x0,u,x0,v構(gòu)成的表達(dá)式，表達(dá)式exp是根據(jù)指令I(lǐng)的指令助記符確定，“∧”是數(shù)理邏輯中的“合取”連接詞，“→”是“隱含”連接詞。 3.根據(jù)權(quán)利要求1所述的一種順序匯編指令程序驗(yàn)證方法，其特征是，順序匯編指令程序語義規(guī)約的方法如下：