[發(fā)明專利]一種匯編程序的形式驗證框架在審
| 申請?zhí)枺?/td> | 201410591523.8 | 申請日： | 2014-10-30 |
| 公開（公告）號： | CN105630568A | 公開（公告）日： | 2016-06-01 |
| 發(fā)明（設(shè)計）人： | 陳偉男 | 申請（專利權(quán)）人： | 鎮(zhèn)江華揚(yáng)信息科技有限公司 |
| 主分類號： | G06F9/45 | 分類號： | G06F9/45 |
| 代理公司： | 暫無信息 | 代理人： | 暫無信息 |
| 地址： | 212009 江蘇省鎮(zhèn)江市新*** | 國省代碼： | 江蘇;32 |
| 權(quán)利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關(guān)鍵詞： | 一種 匯編程序 形式 驗證 框架 | ||
1.一種匯編程序的形式驗證框架其特征主要包括斷言與規(guī)范語言、合式公式、推理規(guī)則和可靠性證明。
2.根據(jù)權(quán)利要求1中的斷言與規(guī)范語言則是直接使用元邏輯,斷言的類型是State—State—Prop，即斷言是以兩個狀態(tài)為參數(shù)的謂詞，它們分別是所在函數(shù)的初始狀態(tài)和當(dāng)前狀態(tài)．使用函數(shù)初始狀態(tài)便于表達(dá)函數(shù)返回值和參數(shù)初值之間的聯(lián)系，也便于表達(dá)匯編程序的一些特定性質(zhì)。
3.根據(jù)權(quán)利要求1中合式公式則是斷言加到代碼塊、函數(shù)和程序上，形成5個層次的合式公式：合式代碼塊、合式函數(shù)體、合式函數(shù)、合式代碼堆和合式程序。
4.根據(jù)權(quán)利要求1中推理規(guī)則和可靠性證明則是定義了推理規(guī)則之后，要證明這些靜態(tài)推理規(guī)則對TM操作語義的可靠性,它保證良形的程序可以在目標(biāo)機(jī)器上一直安全執(zhí)行。
該專利技術(shù)資料僅供研究查看技術(shù)是否侵權(quán)等信息，商用須獲得專利權(quán)人授權(quán)。該專利全部權(quán)利屬于鎮(zhèn)江華揚(yáng)信息科技有限公司，未經(jīng)鎮(zhèn)江華揚(yáng)信息科技有限公司許可，擅自商用是侵權(quán)行為。如果您想購買此專利、獲得商業(yè)授權(quán)和技術(shù)合作，請聯(lián)系【客服】
本文鏈接：http://www.szxzyx.cn/pat/books/201410591523.8/1.html，轉(zhuǎn)載請聲明來源鉆瓜專利網(wǎng)。
