论文部分内容阅读
在高可信软件的各种性质中，安全性是被关注的重点，其中软件满足安全策略的证明方法是研究的热点之一．文中根据作者所设想的安全程序的设计和证明框架，为类C语言的一个子集设计了一个指针逻辑系统．该逻辑系统是Hoare逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况．它可用来对指针程序进行精确的指针分析，所获得的信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全性验证．该逻辑系统也可用来证明指针程序的其它性质．