面向计算机专业的数理逻辑实验课的教学改革

随着定理证明技术在国内科研院所、大专院校以及企业中的推广,在面向计算机专业的数理逻辑课程中开展基于定理证明器的实验课教学,可以引入更多计算的色彩,调动学生的学习兴趣,对推动数理逻辑教学改革有着积极的作用。

一种基于分离逻辑的块云存储系统验证工具

云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.