小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2013年
7期
1482-1486
,共5页
程序验证%Hoare逻辑%形状图逻辑%程序分析%自定义谓词
程序驗證%Hoare邏輯%形狀圖邏輯%程序分析%自定義謂詞
정서험증%Hoare라집%형상도라집%정서분석%자정의위사
software safety%hoare logic%user-defined predicates%verification%prover
基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.
基于邏輯推理的方法進行程序驗證是形式化程序驗證的研究熱點.目前的自動驗證工具為瞭保證自動性,對描述程序性質的斷言語言都有較多限製,導緻程序的某些遞歸性質難以用斷言語言錶述.本文在一箇麵嚮指針程序、基于先前自行設計的形狀圖邏輯、依賴于自動定理證明工具Z3的自動程序驗證原型繫統上,通過在斷言語言中引入自定義謂詞來增彊斷言語言的錶達能力,使得該原型繫統不僅能自動驗證含操作易變數據結構的程序的性質,也能自動驗證一些不含指針的程序的性質.
기우라집추리적방법진행정서험증시형식화정서험증적연구열점.목전적자동험증공구위료보증자동성,대묘술정서성질적단언어언도유교다한제,도치정서적모사체귀성질난이용단언어언표술.본문재일개면향지침정서、기우선전자행설계적형상도라집、의뢰우자동정리증명공구Z3적자동정서험증원형계통상,통과재단언어언중인입자정의위사래증강단언어언적표체능력,사득해원형계통불부능자동험증함조작역변수거결구적정서적성질,야능자동험증일사불함지침적정서적성질.
