软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2010年
3期
415-426
,共12页
陈意云%李兆鹏%王志芳%华保健
陳意雲%李兆鵬%王誌芳%華保健
진의운%리조붕%왕지방%화보건
软件安全%Hoare逻辑%指针逻辑%携带证明的代码%出具证明的编译器
軟件安全%Hoare邏輯%指針邏輯%攜帶證明的代碼%齣具證明的編譯器
연건안전%Hoare라집%지침라집%휴대증명적대마%출구증명적편역기
software safety%Hoare logic%pointer logic%proof-carrying code%certifying compiler
本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合.
本文改進併擴展先前為驗證指針程序提齣的指針邏輯,主要貢獻是提齣瞭閤法訪問路徑集閤的概唸,極大地簡化瞭訪問路徑上的基本運算,併使得指針邏輯推理規則變得易理解.另外,增加瞭跼部推理規則和函數構造的推理規則,使得指針邏輯可以方便地用于有函數調用的場閤.
본문개진병확전선전위험증지침정서제출적지침라집,주요공헌시제출료합법방문로경집합적개념,겁대지간화료방문로경상적기본운산,병사득지침라집추리규칙변득역리해.령외,증가료국부추리규칙화함수구조적추리규칙,사득지침라집가이방편지용우유함수조용적장합.
