软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2010年
2期
334-343
,共10页
梁红瑾%张昱%陈意云%李兆鹏%华保健
樑紅瑾%張昱%陳意雲%李兆鵬%華保健
량홍근%장욱%진의운%리조붕%화보건
软件安全%Hoare逻辑%指针逻辑
軟件安全%Hoare邏輯%指針邏輯
연건안전%Hoare라집%지침라집
software safety%Hoare logic%pointer logic
为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展,可用来对指针程序进行精确的指针分析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种指针逻辑,使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质证明.
為類C小語言PointerC設計的指針邏輯是Hoare邏輯的一種擴展,可用來對指針程序進行精確的指針分析,以支持指針相等關繫確定的程序的安全性驗證.通過增加相等關繫不確定的指針類型訪問路徑集閤,可擴展這種指針邏輯,使得擴展後的指針邏輯可以應用于有嚮圖等指針相等關繫不確定的抽象數據結構上的指針程序性質證明.
위류C소어언PointerC설계적지침라집시Hoare라집적일충확전,가용래대지침정서진행정학적지침분석,이지지지침상등관계학정적정서적안전성험증.통과증가상등관계불학정적지침류형방문로경집합,가확전저충지침라집,사득확전후적지침라집가이응용우유향도등지침상등관계불학정적추상수거결구상적지침정서성질증명.
