[0133] 本發(fā)明方法對(duì)指令系統(tǒng)中的指令設(shè)計(jì)語(yǔ)義規(guī)則，從比較簡(jiǎn)單的匯編指令的語(yǔ)義規(guī)則、簡(jiǎn)單的單條匯編指令的語(yǔ)義證明腳本的生成方法出發(fā)，利用歸納技術(shù)方法得到整個(gè)順序匯編指令程序語(yǔ)義的規(guī)約和驗(yàn)證腳本生成的方法；本發(fā)明方法可完成自動(dòng)驗(yàn)證，使驗(yàn)證周期大大縮短且減小工作量以及時(shí)間和成本消耗。 [0134] 本領(lǐng)域內(nèi)的技術(shù)人員應(yīng)明白，本申請(qǐng)的實(shí)施例可提供為方法、系統(tǒng)、或計(jì)算機(jī)程序產(chǎn)品。因此，本申請(qǐng)可采用完全硬件實(shí)施例、完全軟件實(shí)施例、或結(jié)合軟件和硬件方面的實(shí)施例的形式。而且，本申請(qǐng)可采用在一個(gè)或多個(gè)其中包含有計(jì)算機(jī)可用程序代碼的計(jì)算機(jī)可用存儲(chǔ)介質(zhì)(包括但不限于磁盤存儲(chǔ)器、CD-ROM、光學(xué)存儲(chǔ)器等)上實(shí)施的計(jì)算機(jī)程序產(chǎn)品的形式。 [0135] 本申請(qǐng)是參照根據(jù)本申請(qǐng)實(shí)施例的方法、設(shè)備(系統(tǒng))、和計(jì)算機(jī)程序產(chǎn)品的流程圖和/或方框圖來(lái)描述的。應(yīng)理解可由計(jì)算機(jī)程序指令實(shí)現(xiàn)流程圖和/或方框圖中的每一流程和/或方框、以及流程圖和/或方框圖中的流程和/或方框的結(jié)合。可提供這些計(jì)算機(jī)程序指令到通用計(jì)算機(jī)、專用計(jì)算機(jī)、嵌入式處理機(jī)或其他可編程數(shù)據(jù)處理設(shè)備的處理器以產(chǎn)生一個(gè)機(jī)器，使得通過(guò)計(jì)算機(jī)或其他可編程數(shù)據(jù)處理設(shè)備的處理器執(zhí)行的指令產(chǎn)生用于實(shí)現(xiàn)在流程圖一個(gè)流程或多個(gè)流程和/或方框圖一個(gè)方框或多個(gè)方框中指定的功能的裝置。 [0136] 這些計(jì)算機(jī)程序指令也可存儲(chǔ)在能引導(dǎo)計(jì)算機(jī)或其他可編程數(shù)據(jù)處理設(shè)備以特定方式工作的計(jì)算機(jī)可讀存儲(chǔ)器中，使得存儲(chǔ)在該計(jì)算機(jī)可讀存儲(chǔ)器中的指令產(chǎn)生包括指令裝置的制造品，該指令裝置實(shí)現(xiàn)在流程圖一個(gè)流程或多個(gè)流程和/或方框圖一個(gè)方框或多個(gè)方框中指定的功能。 [0137] 這些計(jì)算機(jī)程序指令也可裝載到計(jì)算機(jī)或其他可編程數(shù)據(jù)處理設(shè)備上，使得在計(jì)算機(jī)或其他可編程設(shè)備上執(zhí)行一系列操作步驟以產(chǎn)生計(jì)算機(jī)實(shí)現(xiàn)的處理，從而在計(jì)算機(jī)或其他可編程設(shè)備上執(zhí)行的指令提供用于實(shí)現(xiàn)在流程圖一個(gè)流程或多個(gè)流程和/或方框圖一個(gè)方框或多個(gè)方框中指定的功能的步驟。 [0138] 以上結(jié)合附圖對(duì)本發(fā)明的實(shí)施例進(jìn)行了描述，但是本發(fā)明并不局限于上述的具體實(shí)施方式，上述的具體實(shí)施方式僅僅是示意性的，而不是限制性的，本領(lǐng)域的普通技術(shù)人員在本發(fā)明的啟示下，在不脫離本發(fā)明宗旨和權(quán)利要求所保護(hù)的范圍情況下，還可做出很多形式，這些均屬于本發(fā)明的保護(hù)之內(nèi)。