[0026] sj-1·a1＝expj-1，1(x1，x2，...，xM)∧…∧sj-1·aM＝expj-1，M(x1，x2，…，xM)； [0027] 其中expj-1，k(x1，x2，...，xM)，k＝1，...，M是由x1，x2，...，xM構(gòu)成的表示式； [0028] 指令執(zhí)行后所有操作數(shù)的值用一個(gè)邏輯公式Qj(s0，sj)表示，表達(dá)式如下：sj·ak＝expj，k(x1，x2，...，xM)，k＝1，2，...，M； [0029] 第j條指令執(zhí)行語義規(guī)約要證明的是： [0030] Qj-1(s0，sj-1)∧(sj＝Ijsj-1)→Qj(s0，sj)； [0031] 找到指令的源操作數(shù)au和目標(biāo)操作數(shù)av，確定公式(sj＝Ijsj-1)中的sj·av＝exp(expj-1，u(x1，x2，...，xM)，expj-1，v(x1，x2，...，xM))，根據(jù)指令I(lǐng)j的語句規(guī)則直接給出命題Qj-1(s0，sj-1)∧(sj＝Ijsj-1)→Qj(s0，sj)的證明腳本； [0032] 以此類推，證明QN-l(s0，sj-1)∧(sN＝INsN-1)→QN(s0，sj)； [0033] 根據(jù)前面證明的命題，給出最終命題Q0(s0)∧(sN＝ININ-1…I1s0)→QN(s0，sj)的證明腳本。 [0034] 進(jìn)一步地，所述語義規(guī)則用于描述將指令執(zhí)行后系統(tǒng)的狀態(tài)向量s1中指令的目標(biāo)操作數(shù)分量表示成由指令執(zhí)行前系統(tǒng)的狀態(tài)向量s0中源操作數(shù)分量構(gòu)成的表達(dá)式的公式； [0035] 在另一個(gè)方面，本發(fā)明提供了一種順序匯編指令程序驗(yàn)證系統(tǒng)，包括： [0036] 指令語義規(guī)則建立模塊、順序匯編指令程序狀態(tài)空間建立模塊、匯編指令語義規(guī)約模塊和語義證明腳本生成模塊； [0037] 所述指令語義規(guī)則建立模塊，用于對(duì)指令系統(tǒng)中用匯編語句表示的每一條指令建立一個(gè)語義規(guī)則； [0038] 順序匯編指令程序狀態(tài)空間建立模塊，用于建立順序匯編指令程序狀態(tài)空間、依次獲取順序匯編指令程序中操作數(shù)的地址a1，a2，...，aM、長(zhǎng)度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)向量空間； [0039] 所述匯編指令語義規(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ù)； [0040] 所述語義證明腳本生成模塊，用于依次對(duì)順序匯編指令程序中的指令根據(jù)指令的語義規(guī)則、指令執(zhí)行前的程序的狀態(tài)向量，生成指令執(zhí)行后新的狀態(tài)向量為規(guī)約出來的狀態(tài)向量ej，1，ej，2，……，ej，M的證明腳本。 [0041] 本發(fā)明所達(dá)到的有益技術(shù)效果： [0042] 本發(fā)明從比較簡(jiǎn)單的匯編指令的語義規(guī)則、簡(jiǎn)單的單條匯編指令的語義證明腳本的生成方法出發(fā)，利用歸納技術(shù)方法得到整個(gè)順序匯編指令程序語義的規(guī)約和驗(yàn)證腳本生成的方法； [0043] 本發(fā)明提出了形式化驗(yàn)證中部分工作的自動(dòng)化的方法，可以大大減少形式化工作的工作量。 附圖說明 [0044] 圖1是本發(fā)明具體實(shí)施例順序匯編指令程序驗(yàn)證方法流程圖； [0045] 圖2是本發(fā)明具體實(shí)施例順序匯編指令程序驗(yàn)證系統(tǒng)結(jié)構(gòu)示意圖； [0046] 圖3是本發(fā)明具體實(shí)施例順序匯編指令程序驗(yàn)證系統(tǒng)結(jié)構(gòu)示意圖。 具體實(shí)施方式 [0047] 下面對(duì)本發(fā)明作進(jìn)一步描述。以下實(shí)施方式僅用于更加清楚地說明本發(fā)明的技術(shù)方案，而不能以此來限制本發(fā)明的保護(hù)范圍。 [0048] 圖1是本發(fā)明具體實(shí)施例順序匯編指令程序驗(yàn)證方法流程圖；圖1示出了一種順序匯編指令程序驗(yàn)方法，包括： [0049] (1)建立指令語義規(guī)則： [0050] 建立指令語義規(guī)則：對(duì)指令系統(tǒng)中用匯編語句表示的每一條指令建立一個(gè)語義規(guī)則； [0051] 在優(yōu)選地實(shí)施例中建立指令語義規(guī)則方法如下： [0052] 指令I(lǐng)表達(dá)式如下：指令助記符源操作數(shù)，目標(biāo)操作數(shù) [0053] 指令執(zhí)行前的狀態(tài)向量s0表示為：s0·aj＝x0，j，j＝1，2，…，M； [0054] 指令執(zhí)行后的狀態(tài)向量s1表示為：s1·aj＝xl，j，j＝1，2，…，M； [0055] 其中aj程序的工作集中第j個(gè)操作數(shù)的地址，x0，j表示指令執(zhí)行前地址為aj的操作數(shù)的值，x1，j表示指令執(zhí)行后地址為aj的操作數(shù)的值，M是操作數(shù)的總數(shù)。 [0056] 指令I(lǐng)的語義規(guī)則為：

假定程序的第j-1條指令后所有操作數(shù)的值已經(jīng)規(guī)約為x1，x2,…,xM的表達(dá)式ej-1,1,ej-1,2,……,ej-1,M，第j條指令I(lǐng)j的語義為： s1(e+i)＝expi(s0(b),…,s0(b+u-1),s0(e),…,s0(e+u-1)),i＝0,…,u-1,???(1-1)s1(d)＝s0(d),對(duì)所有的d≠e,…,d≠e+u-1等式成立,???(1-2) 其中b是源操作數(shù)地址，e是目標(biāo)操作數(shù)地址；s0是指令執(zhí)行前的狀態(tài)向量；s1是指令執(zhí)行后的狀態(tài)向量；u是機(jī)器字長(zhǎng)；si(d)表示狀態(tài)向量si在地址d一個(gè)字節(jié)上的數(shù)值，這里i＝0或1；expi(…)，表示的是由括號(hào)中的參數(shù)構(gòu)成的表達(dá)式，其中i＝0,…,u-1；根據(jù)操作數(shù)的地址和長(zhǎng)度，為s0(b),…,s0(b+u-1),s0(e),…,s0(e+u-1)在ej-1,1,?ej-1,2,……,ej-1,M找到對(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。 4.根據(jù)權(quán)利要求1所述的一種順序匯編指令程序驗(yàn)證方法，其特征是，語義證明腳本生成方法是： 為程序執(zhí)行前初始狀態(tài)向量s0＝(x1，x2,…,xM)建立一個(gè)表示其特征的謂詞公式：Q0(s0)＝“a1＝x1,…,aM＝xM,”； 在第j條指令執(zhí)行前，程序的狀態(tài)向量與操作數(shù)的初始值的之間的關(guān)系用一個(gè)邏輯公式Qj-1(s0,sj-1)表示，表達(dá)式如下： sj-1.a1＝expj-1,1(x1,x2,…,xM)∧…∧sj-1.aM＝expj-1,M(x1,x2,…,xM)； 其中sj-1是指令I(lǐng)j-1執(zhí)行前的狀態(tài)向量；expj-1,k(x1,x2,…,xM),k＝1,…,M是由x1,x2,…,xM構(gòu)成的表示式； 指令執(zhí)行后所有操作數(shù)的值所滿足的條件用一個(gè)邏輯公式Qj(s0,sj)表示，表達(dá)式如下：sj.ak＝expj,k(x1,x2,…,xM),k＝1,2,…,M；其中sj是指令I(lǐng)j-1執(zhí)行后的狀態(tài)向量； expj-1,k()表示狀態(tài)態(tài)向量sj-1的第k個(gè)分量的表達(dá)式； 第j條指令執(zhí)行語義規(guī)約要證明的是： Qj-1(s0,sj-1)∧(sj＝Ij?sj-1)→Qj(s0,sj)；