论文部分内容阅读
介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例，分析了为支持程序验证的若干分离逻辑研究进展，包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容．指出了分离逻辑进一步深入应用所面临的问题和解决方向．
基于分离逻辑的程序验证技术
【摘 要】
：
介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例，分析了为支持程序验证的若干分离逻辑研究进展，包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模
【机 构】
：
南京大学计算机软件新技术国家重点实验室,南京大学计算机科学与技术系
【出 处】
：
软件学报
【发表日期】
：
2009年8期
【基金项目】
：
Supported by the National Natural Science Foundation of China under Grant Nos.60773170, 60721002, 90818022 （国家自然科学基金）, the National High-Tech Research and Development Plan of China under Grant No.2006
其他文献
近年来，为了缓解日益严重的功耗问题，异构并行体系结构已成为超级计算机发展的一个重要趋势．图形处理器（gr印hicsprocessingunit，简称GPU）凭借其超高的计算性能和性能功耗比，作为一
飞行器飞行试验采集的遥测振动信号频段丰富、成分构成复杂,合理有效地解读其包括的时频信息在分析飞行器结构和环境特性方面至关重要;依托经验模态分解（EMD）方法将复杂信号分
日本傀儡政权伪满洲国统治东北之后,日伪政权通过医疗卫生相关政策的实施,批准医疗防疫机构以及医学院校的设立,使得伪满时期新京市的医疗卫生水平有了相当大的提高。透过这
特殊儿童中有很多孩子存在着感觉统合失调的状况,反映到行为上就产生了很多的行为问题,成为特殊儿童较好地适应社区和校园生活的阻碍。文章主要分析特殊儿童感觉统合失调的行
讨论了以基于前缀封闭集合的Heyting代数的直觉解释的线性μ-演算（IμTL）作为描述“假设．保证”的逻辑基础的问题，提出了一个基于IμTL的“假设-保证”规则．该规则比往常应用线性
镇水塔处于地质滑坡地段,南临16.5米高的崖头,沟底常年雨水冲刷,经对涿鹿县镇水塔建筑本体的现存状况及有关文献进行调查、勘测和残损现况原因针对性具体分析的基础上,提出对